Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfrdg4 Structured version   Visualization version   GIF version

Theorem dfrdg4 31727
Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
dfrdg4 rec(𝐹, 𝐴) = (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))

Proof of Theorem dfrdg4
Dummy variables 𝑎 𝑏 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrdg3 31430 . 2 rec(𝐹, 𝐴) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2 an12 837 . . . . . . . 8 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
3 df-fn 5855 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4 ancom 466 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5 eqcom 2628 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
65anbi1i 730 . . . . . . . . . 10 ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
73, 4, 63bitri 286 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
87anbi1i 730 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
9 anass 680 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
102, 8, 93bitri 286 . . . . . . 7 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1110exbii 1771 . . . . . 6 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
12 vex 3192 . . . . . . . 8 𝑓 ∈ V
1312dmex 7053 . . . . . . 7 dom 𝑓 ∈ V
14 eleq1 2686 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15 raleq 3130 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
1614, 15anbi12d 746 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1716anbi2d 739 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1813, 17ceqsexv 3231 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1911, 18bitri 264 . . . . 5 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
20 df-rex 2913 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
21 eldif 3569 . . . . . 6 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ (𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))))
22 elin 3779 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
2312elfuns 31691 . . . . . . . . 9 (𝑓 Funs ↔ Fun 𝑓)
2412elima 5435 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
25 df-rex 2913 . . . . . . . . . 10 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓))
26 ancom 466 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥Domain𝑓𝑥 ∈ On))
27 vex 3192 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
2827, 12brcnv 5270 . . . . . . . . . . . . . . 15 (𝑥Domain𝑓𝑓Domain𝑥)
2912, 27brdomain 31709 . . . . . . . . . . . . . . 15 (𝑓Domain𝑥𝑥 = dom 𝑓)
3028, 29bitri 264 . . . . . . . . . . . . . 14 (𝑥Domain𝑓𝑥 = dom 𝑓)
3130anbi1i 730 . . . . . . . . . . . . 13 ((𝑥Domain𝑓𝑥 ∈ On) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3226, 31bitri 264 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3332exbii 1771 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On))
3413, 14ceqsexv 3231 . . . . . . . . . . 11 (∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
3533, 34bitri 264 . . . . . . . . . 10 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ dom 𝑓 ∈ On)
3624, 25, 353bitri 286 . . . . . . . . 9 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
3723, 36anbi12i 732 . . . . . . . 8 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3822, 37bitri 264 . . . . . . 7 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3938anbi1i 730 . . . . . 6 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))))
40 brdif 4670 . . . . . . . . . . . . . . 15 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ (𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦))
41 vex 3192 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4212, 41brco 5257 . . . . . . . . . . . . . . . . 17 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
4329anbi1i 730 . . . . . . . . . . . . . . . . . . 19 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
4443exbii 1771 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
45 breq1 4621 . . . . . . . . . . . . . . . . . . 19 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
4613, 45ceqsexv 3231 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4744, 46bitri 264 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4813, 41brcnv 5270 . . . . . . . . . . . . . . . . . 18 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
4913epelc 4992 . . . . . . . . . . . . . . . . . 18 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
5048, 49bitri 264 . . . . . . . . . . . . . . . . 17 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
5142, 47, 503bitri 286 . . . . . . . . . . . . . . . 16 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
5251anbi1i 730 . . . . . . . . . . . . . . 15 ((𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦))
5340, 52bitri 264 . . . . . . . . . . . . . 14 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦))
54 onelon 5712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
55543adant1 1077 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
56 brun 4668 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥))
57 brxp 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}))
58 opelxp 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
5912, 58mpbiran 952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
60 velsn 4169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
6159, 60bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
62 velsn 4169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ { {𝐴}} ↔ 𝑥 = {𝐴})
6361, 62anbi12i 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
6457, 63bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
65 brun 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥))
6627brres 5367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × Limits )))
67 opex 4898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑓, 𝑦⟩ ∈ V
6867, 27brco 5257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥))
69 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑧 ∈ V
7012, 41, 69brimg 31713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩Img𝑧𝑧 = (𝑓𝑦))
7127brbigcup 31674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 Bigcup 𝑥 𝑧 = 𝑥)
7270, 71anbi12i 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7372exbii 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
74 imaexg 7057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 ∈ V → (𝑓𝑦) ∈ V)
7512, 74ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓𝑦) ∈ V
76 unieq 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑦) → 𝑧 = (𝑓𝑦))
7776eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑦) → ( 𝑧 = 𝑥 (𝑓𝑦) = 𝑥))
7875, 77ceqsexv 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ (𝑓𝑦) = 𝑥)
79 eqcom 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑦) = 𝑥𝑥 = (𝑓𝑦))
8078, 79bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ 𝑥 = (𝑓𝑦))
8168, 73, 803bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥𝑥 = (𝑓𝑦))
82 opelxp 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 Limits ))
8312, 82mpbiran 952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 Limits )
8441ellimits 31686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 Limits ↔ Lim 𝑦)
8583, 84bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
8681, 85anbi12ci 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × Limits )) ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8766, 86bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8827brres 5367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × ran Succ)))
8967, 27brco 5257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥))
90 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑎 ∈ V
9167, 90brco 5257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎))
9212, 41, 69brpprod3a 31662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏))
93 3anrot 1041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩))
9490ideq 5239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 I 𝑎𝑓 = 𝑎)
95 equcom 1942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 = 𝑎𝑎 = 𝑓)
9694, 95bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑓 I 𝑎𝑎 = 𝑓)
97 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 𝑏 ∈ V
9897brbigcup 31674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 Bigcup 𝑏 𝑦 = 𝑏)
99 eqcom 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ( 𝑦 = 𝑏𝑏 = 𝑦)
10098, 99bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 Bigcup 𝑏𝑏 = 𝑦)
101 biid 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
10296, 100, 1013anbi123i 1249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
10393, 102bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
1041032exbii 1772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
105 vuniex 6914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑦 ∈ V
106 opeq1 4375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
107106eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
108 opeq2 4376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑏 = 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, 𝑦⟩)
109108eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑦⟩))
11012, 105, 107, 109ceqsex2v 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, 𝑦⟩)
11192, 104, 1103bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧 = ⟨𝑓, 𝑦⟩)
112111anbi1i 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
113112exbii 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
114 opex 4898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑓, 𝑦⟩ ∈ V
115 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ⟨𝑓, 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, 𝑦⟩Apply𝑎))
116114, 115ceqsexv 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, 𝑦⟩Apply𝑎)
11712, 105, 90brapply 31714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟨𝑓, 𝑦⟩Apply𝑎𝑎 = (𝑓 𝑦))
118116, 117bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓 𝑦))
11991, 113, 1183bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎 = (𝑓 𝑦))
12090, 27brfullfun 31724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎FullFun𝐹𝑥𝑥 = (𝐹𝑎))
121119, 120anbi12i 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
122121exbii 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
123 fvex 6163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 𝑦) ∈ V
124 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = (𝑓 𝑦) → (𝐹𝑎) = (𝐹‘(𝑓 𝑦)))
125124eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = (𝑓 𝑦) → (𝑥 = (𝐹𝑎) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
126123, 125ceqsexv 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)) ↔ 𝑥 = (𝐹‘(𝑓 𝑦)))
12789, 122, 1263bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥𝑥 = (𝐹‘(𝑓 𝑦)))
128 opelxp 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
12912, 128mpbiran 952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
13041elrn 5331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
13169, 41brsuccf 31717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧Succ𝑦𝑦 = suc 𝑧)
132131exbii 1771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
133129, 130, 1323bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
134127, 133anbi12ci 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × ran Succ)) ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13588, 134bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13687, 135orbi12i 543 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13765, 136bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13864, 137orbi12i 543 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥) ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
13956, 138bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
140 onzsl 7000 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
141 nlim0 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim ∅
142 limeq 5699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
143141, 142mtbiri 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ Lim 𝑦)
144143intnanrd 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
145 nsuceq0 5769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 suc 𝑧 ≠ ∅
146 neeq2 2853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = ∅ → (suc 𝑧𝑦 ↔ suc 𝑧 ≠ ∅))
147145, 146mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = ∅ → suc 𝑧𝑦)
148147necomd 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
149148neneqd 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
150149nexdv 1861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
151150intnanrd 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
152 ioran 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) ↔ (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
153144, 151, 152sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → ¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
154 orel2 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
155153, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
156 iftrue 4069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
157 unisnif 31701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
158156, 157syl6eqr 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = {𝐴})
159158eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = {𝐴}))
160159biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
161160adantld 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
162155, 161syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
163159biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = {𝐴}))
164163anc2li 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
165 orc 400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
166164, 165syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
167162, 166impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
168 neeq1 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
169145, 168mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧𝑦 ≠ ∅)
170169neneqd 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
171170intnanrd 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
172171rexlimivw 3023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
173 orel1 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
174172, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
175 nlimsucg 6996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ V → ¬ Lim suc 𝑧)
17669, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim suc 𝑧
177 limeq 5699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
178176, 177mtbiri 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
179178rexlimivw 3023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
180179intnanrd 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
181 orel1 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
182180, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
183145neii 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ¬ suc 𝑧 = ∅
184183iffalsei 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))
185 iffalse 4072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧)))
18669, 175, 185mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧))
187184, 186eqtri 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = (𝐹‘(𝑓 suc 𝑧))
188 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
189 unieq 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = suc 𝑧 𝑦 = suc 𝑧)
190189fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = suc 𝑧 → (𝑓 𝑦) = (𝑓 suc 𝑧))
191190fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = suc 𝑧 → (𝐹‘(𝑓 𝑦)) = (𝐹‘(𝑓 suc 𝑧)))
192177, 191ifbieq2d 4088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))
193188, 192ifbieq2d 4088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
194187, 193, 1913eqtr4a 2681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
195194rexlimivw 3023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
196195eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
197196biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
198197adantld 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
199174, 182, 1983syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
200 rexex 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
201196biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝐹‘(𝑓 𝑦))))
202 olc 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
203202olcd 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
204200, 201, 203syl6an 567 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
205199, 204impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
206143con2i 134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ 𝑦 = ∅)
207206intnanrd 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
208207, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
209178exlimiv 1855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
210209con2i 134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
211210intnanrd 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
212 orel2 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
213211, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
214206iffalsed 4074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
215 iftrue 4069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = (𝑓𝑦))
216214, 215eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝑓𝑦))
217216eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝑓𝑦)))
218217biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = (𝑓𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
219218adantld 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → ((Lim 𝑦𝑥 = (𝑓𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
220208, 213, 2193syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
221220adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
222217biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝑓𝑦)))
223222anc2li 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
224 orc 400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
225224olcd 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
226223, 225syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
227226adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
228221, 227impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
229167, 205, 2283jaoi 1388 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
230140, 229sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
231139, 230syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
23255, 231syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
23327, 67brcnv 5270 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
23412, 41, 27brapply 31714 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
235233, 234bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦)))
237232, 236anbi12d 746 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ∧ 𝑥 = (𝑓𝑦))))
238 ancom 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ∧ 𝑥 = (𝑓𝑦)) ↔ (𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
239237, 238syl6bb 276 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
240239exbidv 1847 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
241 df-br 4619 . . . . . . . . . . . . . . . . . . . 20 (𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))
24267elfix 31679 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))) ↔ ⟨𝑓, 𝑦⟩(Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))⟨𝑓, 𝑦⟩)
24367, 67brco 5257 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑓, 𝑦⟩(Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩))
244241, 242, 2433bitri 286 . . . . . . . . . . . . . . . . . . 19 (𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩))
245 fvex 6163 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
246245eqvinc 3317 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
247240, 244, 2463bitr4g 303 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
248247notbid 308 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
2492483expia 1264 . . . . . . . . . . . . . . . 16 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (𝑦 ∈ dom 𝑓 → (¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
250249pm5.32d 670 . . . . . . . . . . . . . . 15 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → ((𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
251 annim 441 . . . . . . . . . . . . . . 15 ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
252250, 251syl6bb 276 . . . . . . . . . . . . . 14 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → ((𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
25353, 252syl5bb 272 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
254253exbidv 1847 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ ∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
255 exnal 1751 . . . . . . . . . . . 12 (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
256254, 255syl6rbb 277 . . . . . . . . . . 11 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦))
25712eldm 5286 . . . . . . . . . . 11 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔ ∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦)
258256, 257syl6bbr 278 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))))
259258con1bid 345 . . . . . . . . 9 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
260 df-ral 2912 . . . . . . . . 9 (∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
261259, 260syl6bbr 278 . . . . . . . 8 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
262261pm5.32i 668 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
263 anass 680 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
264262, 263bitri 264 . . . . . 6 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
26521, 39, 2643bitri 286 . . . . 5 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
26619, 20, 2653bitr4ri 293 . . . 4 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
267266abbi2i 2735 . . 3 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
268267unieqi 4416 . 2 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2691, 268eqtr4i 2646 1 rec(𝐹, 𝐴) = (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wne 2790  wral 2907  wrex 2908  Vcvv 3189  cdif 3556  cun 3557  cin 3558  c0 3896  ifcif 4063  {csn 4153  cop 4159   cuni 4407   class class class wbr 4618   E cep 4988   I cid 4989   × cxp 5077  ccnv 5078  dom cdm 5079  ran crn 5080  cres 5081  cima 5082  ccom 5083  Oncon0 5687  Lim wlim 5688  suc csuc 5689  Fun wfun 5846   Fn wfn 5847  cfv 5852  reccrdg 7457  pprodcpprod 31606   Bigcup cbigcup 31609   Fix cfix 31610   Limits climits 31611   Funs cfuns 31612  Imgcimg 31617  Domaincdomain 31618  Applycapply 31620  Succcsuccf 31623  FullFuncfullfn 31625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-symdif 3827  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-txp 31629  df-pprod 31630  df-bigcup 31633  df-fix 31634  df-limits 31635  df-funs 31636  df-singleton 31637  df-singles 31638  df-image 31639  df-cart 31640  df-img 31641  df-domain 31642  df-cup 31644  df-succf 31647  df-apply 31648  df-funpart 31649  df-fullfun 31650
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator