Theorem lamapp2 ≪ | index | src | ≫ 

theorem lamapp2 (A F: set) {x: nat}:
  $ (\ x, F @ x) |` A == F <-> isfun F /\ Dom F == A $;
StepHypRefExpression
1 resisf 
isfun (\ x, F @ x) -> isfun ((\ x, F @ x) |` A)
2 lamisf 
isfun (\ x, F @ x)
3 1, 2 ax_mp 
isfun ((\ x, F @ x) |` A)
4 isfeq 
(\ x, F @ x) |` A == F -> (isfun ((\ x, F @ x) |` A) <-> isfun F)
5 3, 4 mpbii 
(\ x, F @ x) |` A == F -> isfun F
6 dmeq 
(\ x, F @ x) |` A == F -> Dom ((\ x, F @ x) |` A) == Dom F
7 dmreslam 
Dom ((\ x, F @ x) |` A) == A
8 7 a1i 
(\ x, F @ x) |` A == F -> Dom ((\ x, F @ x) |` A) == A
9 6, 8 eqstr3d 
(\ x, F @ x) |` A == F -> Dom F == A
10 5, 9 iand 
(\ x, F @ x) |` A == F -> isfun F /\ Dom F == A
11 prelres 
y, z e. (\ x, F @ x) |` A <-> y, z e. \ x, F @ x /\ y e. A
12 anr 
isfun F /\ Dom F == A -> Dom F == A
13 12 eleq2d 
isfun F /\ Dom F == A -> (y e. Dom F <-> y e. A)
14 13 aneq2d 
isfun F /\ Dom F == A -> (y, z e. \ x, F @ x /\ y e. Dom F <-> y, z e. \ x, F @ x /\ y e. A)
15 impexp 
y, z e. \ x, F @ x /\ y e. Dom F -> y, z e. F <-> y, z e. \ x, F @ x -> y e. Dom F -> y, z e. F
16 eqeq1 
p = y, z -> (p = x, F @ x <-> y, z = x, F @ x)
17 16 exeqd 
p = y, z -> (E. x p = x, F @ x <-> E. x y, z = x, F @ x)
18 17 elabe 
y, z e. {p | E. x p = x, F @ x} <-> E. x y, z = x, F @ x
19 18 conv lam 
y, z e. \ x, F @ x <-> E. x y, z = x, F @ x
20 prth 
y, z = x, F @ x <-> y = x /\ z = F @ x
21 anl 
y = x /\ z = F @ x -> y = x
22 20, 21 sylbi 
y, z = x, F @ x -> y = x
23 22 eleq1d 
y, z = x, F @ x -> (y e. Dom F <-> x e. Dom F)
24 eleq1 
y, z = x, F @ x -> (y, z e. F <-> x, F @ x e. F)
25 23, 24 imeqd 
y, z = x, F @ x -> (y e. Dom F -> y, z e. F <-> x e. Dom F -> x, F @ x e. F)
26 eldm 
x e. Dom F <-> E. y x, y e. F
27 anll 
isfun F /\ Dom F == A /\ x, y e. F -> isfun F
28 anr 
isfun F /\ Dom F == A /\ x, y e. F -> x, y e. F
29 27, 28 isfappd 
isfun F /\ Dom F == A /\ x, y e. F -> F @ x = y
30 29 preq2d 
isfun F /\ Dom F == A /\ x, y e. F -> x, F @ x = x, y
31 30 eleq1d 
isfun F /\ Dom F == A /\ x, y e. F -> (x, F @ x e. F <-> x, y e. F)
32 31, 28 mpbird 
isfun F /\ Dom F == A /\ x, y e. F -> x, F @ x e. F
33 32 eexda 
isfun F /\ Dom F == A -> E. y x, y e. F -> x, F @ x e. F
34 26, 33 syl5bi 
isfun F /\ Dom F == A -> x e. Dom F -> x, F @ x e. F
35 25, 34 syl5ibrcom 
isfun F /\ Dom F == A -> y, z = x, F @ x -> y e. Dom F -> y, z e. F
36 35 eexd 
isfun F /\ Dom F == A -> E. x y, z = x, F @ x -> y e. Dom F -> y, z e. F
37 19, 36 syl5bi 
isfun F /\ Dom F == A -> y, z e. \ x, F @ x -> y e. Dom F -> y, z e. F
38 15, 37 sylibr 
isfun F /\ Dom F == A -> y, z e. \ x, F @ x /\ y e. Dom F -> y, z e. F
39 anr 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> x = y
40 39 appeq2d 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> F @ x = F @ y
41 an3l 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> isfun F
42 anlr 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> y, z e. F
43 41, 42 isfappd 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> F @ y = z
44 40, 43 eqtrd 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> F @ x = z
45 39, 44 preqd 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> x, F @ x = y, z
46 45 eqcomd 
isfun F /\ Dom F == A /\ y, z e. F /\ x = y -> y, z = x, F @ x
47 46 iexde 
isfun F /\ Dom F == A /\ y, z e. F -> E. x y, z = x, F @ x
48 19, 47 sylibr 
isfun F /\ Dom F == A /\ y, z e. F -> y, z e. \ x, F @ x
49 preldm 
y, z e. F -> y e. Dom F
50 49 anwr 
isfun F /\ Dom F == A /\ y, z e. F -> y e. Dom F
51 48, 50 iand 
isfun F /\ Dom F == A /\ y, z e. F -> y, z e. \ x, F @ x /\ y e. Dom F
52 51 exp 
isfun F /\ Dom F == A -> y, z e. F -> y, z e. \ x, F @ x /\ y e. Dom F
53 38, 52 ibid 
isfun F /\ Dom F == A -> (y, z e. \ x, F @ x /\ y e. Dom F <-> y, z e. F)
54 14, 53 bitr3d 
isfun F /\ Dom F == A -> (y, z e. \ x, F @ x /\ y e. A <-> y, z e. F)
55 11, 54 syl5bb 
isfun F /\ Dom F == A -> (y, z e. (\ x, F @ x) |` A <-> y, z e. F)
56 55 eqrd2 
isfun F /\ Dom F == A -> (\ x, F @ x) |` A == F
57 10, 56 ibii 
(\ x, F @ x) |` A == F <-> isfun F /\ Dom F == A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)