HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem tz9.12lem3 4633
Description: Lemma for tz9.12 4634.
Hypotheses
Ref Expression
tz9.12lem.1 |- A e. V
tz9.12lem.2 |- F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
Assertion
Ref Expression
tz9.12lem3 |- (A.x e. A E.y e. On x e. (R1` y) -> A e. (R1` suc suc U.(F"A)))
Distinct variable groups:   x,y,z,w,v,A   x,F,y
Proof of Theorem tz9.12lem3
StepHypRef Expression
1 fveq2 3709 . . . . . . . . . . . . . 14 |- (v = y -> (R1` v) = (R1` y))
21eleq2d 1533 . . . . . . . . . . . . 13 |- (v = y -> (x e. (R1` v) <-> x e. (R1` y)))
32rcla4ev 1868 . . . . . . . . . . . 12 |- ((y e. On /\ x e. (R1` y)) -> E.v e. On x e. (R1` v))
4 rabn0 2282 . . . . . . . . . . . 12 |- ({v e. On | x e. (R1` v)} =/= (/) <-> E.v e. On x e. (R1` v))
53, 4sylibr 200 . . . . . . . . . . 11 |- ((y e. On /\ x e. (R1` y)) -> {v e. On | x e. (R1` v)} =/= (/))
6 tz9.12lem.2 . . . . . . . . . . . . . . . 16 |- F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
76eleq2i 1530 . . . . . . . . . . . . . . 15 |- (<.x, y>. e. F <-> <.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
8 visset 1804 . . . . . . . . . . . . . . . 16 |- x e. V
9 visset 1804 . . . . . . . . . . . . . . . 16 |- y e. V
10 eleq1 1526 . . . . . . . . . . . . . . . . . . 19 |- (z = x -> (z e. (R1` v) <-> x e. (R1` v)))
1110rabbisdv 1798 . . . . . . . . . . . . . . . . . 18 |- (z = x -> {v e. On | z e. (R1` v)} = {v e. On | x e. (R1` v)})
1211inteqd 2528 . . . . . . . . . . . . . . . . 17 |- (z = x -> |^|{v e. On | z e. (R1` v)} = |^|{v e. On | x e. (R1` v)})
1312eqeq2d 1478 . . . . . . . . . . . . . . . 16 |- (z = x -> (w = |^|{v e. On | z e. (R1` v)} <-> w = |^|{v e. On | x e. (R1` v)}))
14 eqeq1 1473 . . . . . . . . . . . . . . . 16 |- (w = y -> (w = |^|{v e. On | x e. (R1` v)} <-> y = |^|{v e. On | x e. (R1` v)}))
158, 9, 13, 14opelopab 2809 . . . . . . . . . . . . . . 15 |- (<.x, y>. e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} <-> y = |^|{v e. On | x e. (R1` v)})
167, 15bitr 173 . . . . . . . . . . . . . 14 |- (<.x, y>. e. F <-> y = |^|{v e. On | x e. (R1` v)})
1716exbii 1047 . . . . . . . . . . . . 13 |- (E.y<.x, y>. e. F <-> E.y y = |^|{v e. On | x e. (R1` v)})
188eldm2 3297 . . . . . . . . . . . . 13 |- (x e. dom F <-> E.y<.x, y>. e. F)
19 isset 1805 . . . . . . . . . . . . 13 |- (|^|{v e. On | x e. (R1` v)} e. V <-> E.y y = |^|{v e. On | x e. (R1` v)})
2017, 18, 193bitr4 183 . . . . . . . . . . . 12 |- (x e. dom F <-> |^|{v e. On | x e. (R1` v)} e. V)
21 intex 2719 . . . . . . . . . . . 12 |- ({v e. On | x e. (R1` v)} =/= (/) <-> |^|{v e. On | x e. (R1` v)} e. V)
2220, 21bitr4 176 . . . . . . . . . . 11 |- (x e. dom F <-> {v e. On | x e. (R1` v)} =/= (/))
235, 22sylibr 200 . . . . . . . . . 10 |- ((y e. On /\ x e. (R1` y)) -> x e. dom F)
24 funopabeq 3535 . . . . . . . . . . . 12 |- Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}
25 funeq 3521 . . . . . . . . . . . . 13 |- (F = {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} -> (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}))
266, 25ax-mp 7 . . . . . . . . . . . 12 |- (Fun F <-> Fun {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
2724, 26mpbir 190 . . . . . . . . . . 11 |- Fun F
28 funfvima 3837 . . . . . . . . . . 11 |- ((Fun F /\ x e. dom F) -> (x e. A -> (F` x) e. (F"A)))
2927, 28mpan 693 . . . . . . . . . 10 |- (x e. dom F -> (x e. A -> (F` x) e. (F"A)))
3023, 29syl 10 . . . . . . . . 9 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (F` x) e. (F"A)))
31 tz9.12lem.1 . . . . . . . . . . . . 13 |- A e. V
3231, 6tz9.12lem1 4631 . . . . . . . . . . . 12 |- (F"A) (_ On
33 onsucuni 3075 . . . . . . . . . . . 12 |- ((F"A) (_ On -> (F"A) (_ suc U.(F"A))
3432, 33ax-mp 7 . . . . . . . . . . 11 |- (F"A) (_ suc U.(F"A)
3534sseli 2055 . . . . . . . . . 10 |- ((F` x) e. (F"A) -> (F` x) e. suc U.(F"A))
3631, 6tz9.12lem2 4632 . . . . . . . . . . 11 |- suc U.(F"A) e. On
37 r1ord2 4628 . . . . . . . . . . 11 |- (suc U.(F"A) e. On -> ((F` x) e. suc U.(F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A))))
3836, 37ax-mp 7 . . . . . . . . . 10 |- ((F` x) e. suc U.(F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
3935, 38syl 10 . . . . . . . . 9 |- ((F` x) e. (F"A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
4030, 39syl6 22 . . . . . . . 8 |- ((y e. On /\ x e. (R1` y)) -> (x e. A -> (R1` (F` x)) (_ (R1` suc U.(F"A))))
4140imp 350 . . . . . . 7 |- (((y e. On /\ x e. (R1` y)) /\ x e. A) -> (R1` (F` x)) (_ (R1` suc U.(F"A)))
4212fvopabg 3770 . . . . . . . . . . . . 13 |- ((x e. V /\ |^|{v e. On | x e. (R1` v)} e. V) -> ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x) = |^|{v e. On | x e. (R1` v)})
438, 42mpan 693 . . . . . . . . . . . 12 |- (|^|{v e. On | x e. (R1` v)} e. V -> ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x) = |^|{v e. On | x e. (R1` v)})
446fveq1i 3710 . . . . . . . . . . . 12 |- (F` x) = ({<.z, w>. | w = |^|{v e. On | z e. (R1` v)}}` x)
4543, 44syl5eq 1511 . . . . . . . . . . 11 |- (|^|{v e. On | x e. (R1` v)} e. V -> (F` x) = |^|{v e. On | x e. (R1` v)})
4621, 45sylbi 199 . . . . . . . . . 10 |- ({v e. On | x e. (R1` v)} =/= (/) -> (F` x) = |^|{v e. On | x e. (R1` v)})
47 ssrab2 2121 . . . . . . . . . . 11 |- {v e. On | x e. (R1` v)} (_ On
48 onint 2996 . . . . . . . . . . 11 |- (({v e. On | x e. (R1` v)} (_ On /\ {v e. On | x e. (R1` v)} =/= (/)) -> |^|{v e. On | x e. (R1` v)} e. {v e. On | x e. (R1` v)})
4947, 48mpan 693 . . . . . . . . . 10 |- ({v e. On | x e. (R1` v)} =/= (/) -> |^|{v e. On | x e. (R1` v)} e. {v e. On | x e. (R1` v)})
5046, 49eqeltrd 1540 . . . . . . . . 9 |- ({v e. On | x e. (R1` v)} =/= (/) -> (F` x) e. {v e. On | x e. (R1` v)})
51 hbrab1 1764 . . . . . . . . . . . . . . . 16 |- (w e. {v e. On | z e. (R1` v)} -> A.v w e. {v e. On | z e. (R1` v)})
5251hbint 2533 . . . . . . . . . . . . . . 15 |- (w e. |^|{v e. On | z e. (R1` v)} -> A.v w e. |^|{v e. On | z e. (R1` v)})
5352hbeleq 1559 . . . . . . . . . . . . . 14 |- (w = |^|{v e. On | z e. (R1` v)} -> A.v w = |^|{v e. On | z e. (R1` v)})
5453hbopab 2801 . . . . . . . . . . . . 13 |- (y e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}} -> A.v y e. {<.z, w>. | w = |^|{v e. On | z e. (R1` v)}})
556, 54hbxfr 1555 . . . . . . . . . . . 12 |- (y e. F -> A.v y e. F)
56 ax-17 968 . . . . . . . . . . . 12 |- (y e. x -> A.v y e. x)
5755, 56hbfv 3714 . . . . . . . . . . 11 |- (y e. (F` x) -> A.v y e. (F` x))
58 ax-17 968 . . . . . . . . . . 11 |- (y e. On -> A.v y e. On)
59 ax-17 968 . . . . . . . . . . . . 13 |- (y e. R1 -> A.v y e. R1)
6059, 57hbfv 3714 . . . . . . . . . . . 12 |- (y e. (R1` (F` x)) -> A.v y e. (R1` (F` x)))
6156, 60hbel 1558 . . . . . . . . . . 11 |- (x e. (R1` (F` x)) -> A.v x e. (R1` (F` x)))
62 fveq2 3709 . . . . . . . . . . . 12 |- (v = (F` x) -> (R1` v) = (R1` (F` x