HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem brdom7disj 5966
Description: An equivalence to a dominance relation for disjoint sets.
Hypotheses
Ref Expression
brdom7disj.1 |- A e. _V
brdom7disj.2 |- B e. _V
brdom7disj.3 |- (A i^i B) = (/)
Assertion
Ref Expression
brdom7disj |- (A ~<_ B <-> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
Distinct variable groups:   x,f,y,A   B,f,x,y
Proof of Theorem brdom7disj
StepHypRef Expression
1 brdom7disj.1 . . 3 |- A e. _V
2 brdom7disj.2 . . 3 |- B e. _V
31, 2brdom4 5965 . 2 |- (A ~<_ B <-> E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx))
4 snex 3492 . . . . . . . . 9 |- {{z, w}} e. _V
5 simpl 346 . . . . . . . . . . 11 |- ((v = {z, w} /\ <.z, w>. e. g) -> v = {z, w})
65ss2abi 2679 . . . . . . . . . 10 |- {v | (v = {z, w} /\ <.z, w>. e. g)} C_ {v | v = {z, w}}
7 df-sn 3049 . . . . . . . . . 10 |- {{z, w}} = {v | v = {z, w}}
86, 7sseqtr4i 2650 . . . . . . . . 9 |- {v | (v = {z, w} /\ <.z, w>. e. g)} C_ {{z, w}}
94, 8ssexi 3456 . . . . . . . 8 |- {v | (v = {z, w} /\ <.z, w>. e. g)} e. _V
102, 9abrexex2 4847 . . . . . . 7 |- {v | E.z e. B (v = {z, w} /\ <.z, w>. e. g)} e. _V
111, 10abrexex2 4847 . . . . . 6 |- {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} e. _V
12 ax-17 1317 . . . . . . . . 9 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> A.y f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})
13 eleq2 1958 . . . . . . . . . 10 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ({x, y} e. f <-> {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
1413anbi2d 678 . . . . . . . . 9 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ((y e. A /\ {x, y} e. f) <-> (y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
1512, 14mobid 1800 . . . . . . . 8 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (E*y(y e. A /\ {x, y} e. f) <-> E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
1615ralbidv 2123 . . . . . . 7 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (A.x e. B E*y(y e. A /\ {x, y} e. f) <-> A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
17 eleq2 1958 . . . . . . . . 9 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ({y, x} e. f <-> {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
1817rexbidv 2124 . . . . . . . 8 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (E.y e. B {y, x} e. f <-> E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
1918ralbidv 2123 . . . . . . 7 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (A.x e. A E.y e. B {y, x} e. f <-> A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
2016, 19anbi12d 690 . . . . . 6 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ((A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f) <-> (A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) /\ A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
2111, 20cla4ev 2371 . . . . 5 |- ((A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) /\ A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) -> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
22 ax-17 1317 . . . . . . 7 |- (x e. B -> A.y x e. B)
23 incom 2787 . . . . . . . . . . . . . . . . . 18 |- (B i^i A) = (A i^i B)
24 brdom7disj.3 . . . . . . . . . . . . . . . . . 18 |- (A i^i B) = (/)
2523, 24eqtri 1908 . . . . . . . . . . . . . . . . 17 |- (B i^i A) = (/)
26 disjne 2919 . . . . . . . . . . . . . . . . 17 |- (((B i^i A) = (/) /\ x e. B /\ w e. A) -> x =/= w)
2725, 26mp3an1 1178 . . . . . . . . . . . . . . . 16 |- ((x e. B /\ w e. A) -> x =/= w)
28 visset 2295 . . . . . . . . . . . . . . . . 17 |- x e. _V
29 visset 2295 . . . . . . . . . . . . . . . . 17 |- y e. _V
30 visset 2295 . . . . . . . . . . . . . . . . 17 |- z e. _V
31 visset 2295 . . . . . . . . . . . . . . . . 17 |- w e. _V
3228, 29, 30, 31opthpr 3156 . . . . . . . . . . . . . . . 16 |- (x =/= w -> ({x, y} = {z, w} <-> (x = z /\ y = w)))
3327, 32syl 12 . . . . . . . . . . . . . . 15 |- ((x e. B /\ w e. A) -> ({x, y} = {z, w} <-> (x = z /\ y = w)))
34 equcom 1488 . . . . . . . . . . . . . . . 16 |- (x = z <-> z = x)
35 equcom 1488 . . . . . . . . . . . . . . . 16 |- (y = w <-> w = y)
3634, 35anbi12i 540 . . . . . . . . . . . . . . 15 |- ((x = z /\ y = w) <-> (z = x /\ w = y))
3733, 36syl6rbb 596 . . . . . . . . . . . . . 14 |- ((x e. B /\ w e. A) -> ((z = x /\ w = y) <-> {x, y} = {z, w}))
38 df-br 3339 . . . . . . . . . . . . . . 15 |- (zgw <-> <.z, w>. e. g)
3938a1i 8 . . . . . . . . . . . . . 14 |- ((x e. B /\ w e. A) -> (zgw <-> <.z, w>. e. g))
4037, 39anbi12d 690 . . . . . . . . . . . . 13 |- ((x e. B /\ w e. A) -> (((z = x /\ w = y) /\ zgw) <-> ({x, y} = {z, w} /\ <.z, w>. e. g)))
4140rexbidva 2120 . . . . . . . . . . . 12 |- (x e. B -> (E.w e. A ((z = x /\ w = y) /\ zgw) <-> E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g)))
4241rexbidv 2124 . . . . . . . . . . 11 |- (x e. B -> (E.z e. B E.w e. A ((z = x /\ w = y) /\ zgw) <-> E.z e. B E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g)))
43 rexcom 2243 . . . . . . . . . . . 12 |- (E.z e. B E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g) <-> E.w e. A E.z e. B ({x, y} = {z, w} /\ <.z, w>. e. g))
44 zfpair2 3525 . . . . . . . . . . . . 13 |- {x, y} e. _V
45 eqeq1 1890 . . . . . . . . . . . . . . 15 |- (v = {x, y} -> (v = {z, w} <-> {x, y} = {z, w}))
4645anbi1d 679 . . . . . . . . . . . . . 14 |- (v = {x, y} -> ((v = {z, w} /\ <.z, w>. e. g) <-> ({x, y} = {z, w} /\ <.z, w>. e. g)))
47462rexbidv 2141 . . . . . . . . . . . . 13 |- (v = {x, y} -> (E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g) <-> E.w e. A E.z e. B ({x, y} = {z, w} /\ <.z, w>. e. g)))
4844, 47elab 2403 . . . . . . . . . . . 12 |- ({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.w e. A E.z e. B ({x, y} = {z, w} /\ <.z, w>. e. g))
4943, 48bitr4i 193 . . . . . . . . . . 11 |- (E.z e. B E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g) <-> {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})
5042, 49syl6rbb 596 . . . . . . . . . 10 |- (x e. B -> ({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.z e. B E.w e. A ((z = x /\ w = y) /\ zgw)))
5150adantr 425 . . . . . . . . 9 |- ((x e. B /\ y e. A) -> ({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.z e. B E.w e. A ((z = x /\ w = y) /\ zgw)))
52 breq1 3341 . . . . . . . . . 10 |- (z = x -> (zgw <-> xgw))
53 breq2 3342 . . . . . . . . . 10 |- (w = y -> (xgw <-> xgy))
5452, 53ceqsrex2v 2395 . . . . . . . . 9 |- ((x e. B /\ y e. A) -> (E.z e. B E.w e. A ((z = x /\ w = y) /\ zgw) <-> xgy))
5551, 54bitrd 587 . . . . . . . 8 |- ((x e. B /\ y e. A) -> ({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> xgy))
5655pm5.32da 711 . . . . . . 7 |- (x e. B -> ((y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) <-> (y e. A /\ xgy)))
5722, 56mobid 1800 . . . . . 6 |- (x e. B -> (E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) <-> E*y(y e. A /\ xgy)))
5857ralbiia 2133 . . . . 5 |- (A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) <-> A.x e. B E*y(y e. A /\ xgy))
59 disjne 2919 . . . . . . . . . . . . . . . . 17 |- (((B i^i A) = (/) /\ z e. B /\ x e. A) -> z =/= x)
6025, 59mp3an1 1178 . . . . . . . . . . . . . . . 16 |- ((z e. B /\ x e. A) -> z =/= x)
6160ancoms 484 . . . . . . . . . . . . . . 15 |- ((x e. A /\ z e. B) -> z =/= x)
6230, 31, 29, 28opthpr 3156 . . . . . . . . . . . . . . 15 |- (z =/= x -> ({z, w} = {y, x} <-> (z = y /\ w = x)))
6361, 62syl 12 . . . . . . . . . . . . . 14 |- ((x e. A /\ z e. B) -> ({z, w} = {y, x} <-> (z = y /\ w = x)))
64 eqcom 1886 . . . . . . . . . . . . . 14 |- ({y, x} = {z, w} <-> {z, w} = {y, x})
65 ancom 482 . . . . . . . . . . . . . 14 |- ((w = x /\ z = y) <-> (z = y /\ w = x))
6663, 64, 653bitr4g 614 . . . . . . . . . . . . 13 |- ((x e. A /\ z e. B) -> ({y, x} = {z, w} <-> (w = x /\ z = y)))
6738bicomi 189 . . . . . . . . . . . . . 14 |- (<.z, w>. e. g <-> zgw)
6867a1i 8 . . . . . . . . . . . . 13 |- ((x e. A /\ z e. B) -> (<.z, w>. e. g <-> zgw))
6966, 68anbi12d 690 . . . . . . . . . . . 12 |- ((x e. A /\ z e. B) -> (({y, x} = {z, w} /\ <.z, w>. e. g) <-> ((w = x /\ z = y) /\ zgw)))
7069rexbidva 2120 . . . . . . . . . . 11 |- (x e. A -> (E.z e. B ({y, x} = {z, w} /\ <.z, w>. e. g) <-> E.z e. B ((w = x /\ z = y) /\ zgw)))
7170rexbidv 2124 . . . . . . . . . 10 |- (x e. A -> (E.w e. A E.z e. B ({y, x} = {z, w} /\ <.z, w>. e. g) <-> E.w e. A E.z e. B ((w = x /\ z = y) /\ zgw)))
72 zfpair2 3525 . . . . . . . . . . 11 |- {y, x} e. _V
73 eqeq1 1890 . . . . . . . . . . . . 13 |- (v = {y, x} -> (v = {z, w} <-> {y, x} = {z, w}))
7473anbi1d 679 . . . . . . . . . . . 12 |- (v = {y, x} -> ((v = {z, w} /\ <.z, w>. e. g) <-> ({y, x} = {z, w} /\ <.z, w>. e. g)))
75742rexbidv 2141 . . . . . . . . . . 11 |- (v = {y, x} -> (E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g) <-> E.w e. A E.z e. B ({y, x} = {z, w} /\ <.z, w>. e. g)))
7672, 75elab 2403 . . . . . . . . . 10 |- ({y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.w e. A E.z e. B ({y, x} = {z, w} /\ <.z, w>. e. g))
7771, 76syl5bb 591 . . . . . . . . 9 |- (x e. A -> ({y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.w e. A E.z e. B ((w = x /\ z = y) /\ zgw)))
7877adantr 425 . . . . . . . 8 |- ((x e. A /\ y e. B) -> ({y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.w e. A E.z e. B ((w = x /\ z = y) /\ zgw)))
79 breq2 3342 . . . . . . . . 9 |- (w = x -> (zgw <-> zgx))
80 breq1 3341 . . . . . . . . 9 |- (z = y -> (zgx <-> ygx))
8179, 80ceqsrex2v 2395 . . . . . . . 8 |- ((x e. A /\ y e. B) -> (E.w e. A E.z e. B ((w = x /\ z = y) /\ zgw) <-> ygx))
8278, 81bitrd 587 . . . . . . 7 |- ((x e. A /\ y e. B) -> ({y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> ygx))
8382rexbidva 2120 . . . . . 6 |- (x e. A -> (E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> E.y e. B ygx))
8483ralbiia 2133 . . . . 5 |- (A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} <-> A.x e. A E.y e. B ygx)
8521, 58, 84syl2anbr 505 . . . 4 |- ((A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx) -> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
868519.23aiv 1674 . . 3 |- (E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx) -> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
87 df-opab 3396 . . . . . . 7 |- {<.w, z>. | {w, z} e. f} = {v | E.wE.z(v = <.w, z>. /\ {w, z} e. f)}
88 visset 2295 . . . . . . . . 9 |- f e. _V
8988uniex 3794 . . . . . . . 8 |- U.f e. _V
9031prid1 3106 . . . . . . . . . . 11 |- w e. {w, z}
91 elunii 3182 . . . . . . . . . . 11 |- ((w e. {w, z} /\ {w, z} e. f) -> w e. U.f)
9290, 91mpan 759 . . . . . . . . . 10 |- ({w, z} e. f -> w e. U.f)
9392adantl 424 . . . . . . . . 9 |- ((v = <.w, z>. /\ {w, z} e. f) -> w e. U.f)
949319.23aiv 1674 . . . . . . . 8 |- (E.z(v = <.w, z>. /\ {w, z} e. f) -> w e. U.f)
9530prid2 3107 . . . . . . . . . . 11 |- z e. {w, z}
96 elunii 3182 . . . . . . . . . . 11 |- ((z e. {w, z} /\ {w, z} e. f) -> z e. U.f)
9795, 96mpan 759 . . . . . . . . . 10 |- ({w, z} e. f -> z e. U.f)
9897adantl 424 . . . . . . . . 9 |- ((v = <.w, z>. /\ {w, z} e. f) -> z e. U.f)
99 df-sn 3049 . . . . . . . . . . 11 |- {<.w, z>.} = {v | v = <.w, z>.}
100 snex 3492 . . . . . . . . . . 11 |- {<.w, z>.} e. _V
10199, 100eqeltrri 1968 . . . . . . . . . 10 |- {v | v = <.w, z>.} e. _V
102 simpl 346 . . . . . . . . . . 11 |- ((v = <.w, z>. /\ {w, z} e. f) -> v = <.w, z>.)
103102ss2abi 2679 . . . . . . . . . 10 |- {v | (v = <.w, z>. /\ {w, z} e. f)} C_ {v | v = <.w, z>.}
104101, 103ssexi 3456 . . . . . . . . 9 |- {v | (v = <.w, z>. /\ {w, z} e. f)} e. _V
10589, 98, 104abexex 4849 . . . . . . . 8 |- {v | E.z(v = <.w, z>. /\ {w, z} e. f)} e. _V
10689, 94, 105abexex 4849 . . . . . . 7 |- {v | E.wE.z(v = <.w, z>. /\ {w, z} e. f)} e. _V
10787, 106eqeltri 1967 . . . . . 6 |- {<.w, z>. | {w, z} e. f} e. _V
108 ax-17 1317 . . . . . . . . 9 |- (g = {<.w, z>. | {w, z} e. f} -> A.y g = {<.w, z>. | {w, z} e. f})
109 breq 3340 . . . . . . . . . 10 |- (g = {<.w, z>. | {w, z} e. f} -> (xgy <-> x{<.w, z>. | {w, z} e. f}y))
110109anbi2d 678 . . . . . . . . 9 |- (g = {<.w, z>. | {w, z} e. f} -> ((y e. A /\ xgy) <-> (y e. A /\ x{<.w, z>. | {w, z} e. f}y)))
111108, 110mobid 1800 . . . . . . . 8 |- (g = {<.w, z>. | {w, z} e. f} -> (E*y(y e. A /\ xgy) <-> E*y(y e. A /\ x{<.w, z>. | {w, z} e. f}y)))
112111ralbidv 2123 . . . . . . 7 |- (g = {<.w, z>. | {w, z} e. f} -> (A.x e. B E*y(y e. A /\ xgy) <-> A.x e. B E*y(y e. A /\ x{<.w, z>. | {w, z} e. f}y)))
113 breq 3340 . . . . . . . . 9 |- (g = {<.w, z>. | {w, z} e. f} -> (ygx <-> y{<.w, z>. | {w, z} e. f}x))
114113rexbidv 2124 . . . . . . . 8 |- (g = {<.w, z>. | {w, z} e. f} -> (E.y e. B ygx <-> E.y e. B y{<.w, z>. | {w, z} e. f}x))
115114ralbidv 2123 . . . . . . 7 |- (g = {<.w, z>. | {w, z} e. f} -> (A.x e. A E.y e. B ygx <-> A.x e. A E.y e. B y{<.w, z>. | {w, z} e. f}x))
116112, 115anbi12d 690 . . . . . 6 |- (g = {<.w, z>. | {w, z} e. f} -> ((A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx) <-> (A.x e. B E*y(y e. A /\ x{<.w, z>. | {w, z} e. f}y) /\ A.x e. A E.y e. B y{<.w, z>. | {w, z} e. f}x)))
117107, 116cla4ev 2371 . . . . 5 |- ((A.x e. B E*y(y e. A /\ x{<.w, z>. | {w, z} e. f}y) /\ A.x e. A E.y e. B y{<.w, z>. | {w, z} e. f}x) -> E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx))
118 preq1 3098 . . . . . . . . . 10 |- (w = x -> {w, z} = {x, z})
119118eleq1d 1963 . . . . . . . . 9 |- (w = x -> ({w, z} e. f <-> {x, z} e. f))
120 preq2 3099 . . . . . . . . . 10 |- (z = y -> {x, z} = {x, y})
121120eleq1d 1963 . . . . . . . . 9 |- (z = y -> ({x, z} e. f <-> {x, y} e. f))
122 eqid 1884 . . . . . . . . 9 |- {<.w, z>. | {w, z} e. f} = {<.w, z>. | {w, z} e. f}
12328, 29, 119, 121, 122brab 3571 . . . . . . . 8 |- (x{<.w, z>. | {w, z} e. f}y <-> {x, y} e. f)
124123anbi2i 538 . . . . . . 7 |- ((y e. A /\ x{<.w, z>. | {w, z} e. f}y) <-> (y e. A /\ {x, y} e. f))
125124mobii 1801 . . . . . 6 |- (E*y(y e. A /\ x{<.w, z>. | {w, z} e. f}y) <-> E*y(y e. A /\ {x, y} e. f))
126125ralbii 2127 . . . . 5 |- (A.x e. B E*y(y e. A /\ x{<.w, z>. | {w, z} e. f}y) <-> A.x e. B E*y(y e. A /\ {x, y} e. f))
127 preq1 3098 . . . . . . . . 9 |- (w = y -> {w, z} = {y, z})
128127eleq1d 1963 . . . . . . . 8 |- (w = y -> ({w, z} e. f <-> {y, z} e. f))
129 preq2 3099 . . . . . . . . 9 |- (z = x -> {y, z} = {y, x})
130129eleq1d 1963 . . . . . . . 8 |- (z = x -> ({y, z} e. f <-> {y, x} e. f))
13129, 28, 128, 130, 122brab 3571 . . . . . . 7 |- (y{<.w, z>. | {w, z} e. f}x <-> {y, x} e. f)
132131rexbii 2128 . . . . . 6 |- (E.y e. B y{<.w, z>. | {w, z} e. f}x <-> E.y e. B {y, x} e. f)
133132ralbii 2127 . . . . 5 |- (A.x e. A E.y e. B y{<.w, z>. | {w, z} e. f}x <-> A.x e. A E.y e. B {y, x} e. f)
134117, 126, 133syl2anbr 505 . . . 4 |- ((A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f) -> E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx))
13513419.23aiv 1674 . . 3 |- (E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f) -> E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx))
13686, 135impbii 174 . 2 |- (E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx) <-> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
1373, 136bitri 190 1 |- (A ~<_ B <-> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
Colors of variables: wff set class
Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  E*wmo 1772  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592  (/)c0 2875  {csn 3044  {cpr 3045  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395   ~<_ cdom 5424
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-ac 5906
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429
Copyright terms: Public domain