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 32183
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 31826 . 2 rec(𝐹, 𝐴) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2 an12 855 . . . . . . . 8 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
3 df-fn 5929 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4 ancom 465 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5 eqcom 2658 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
65anbi1i 731 . . . . . . . . . 10 ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
73, 4, 63bitri 286 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
87anbi1i 731 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
9 anass 682 . . . . . . . 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 1814 . . . . . 6 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
12 vex 3234 . . . . . . . 8 𝑓 ∈ V
1312dmex 7141 . . . . . . 7 dom 𝑓 ∈ V
14 eleq1 2718 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15 raleq 3168 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
1614, 15anbi12d 747 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1716anbi2d 740 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1813, 17ceqsexv 3273 . . . . . 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 2947 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
21 eldif 3617 . . . . . 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 3829 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
2312elfuns 32147 . . . . . . . . 9 (𝑓 Funs ↔ Fun 𝑓)
2412elima 5506 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
25 df-rex 2947 . . . . . . . . . 10 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓))
26 ancom 465 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥Domain𝑓𝑥 ∈ On))
27 vex 3234 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
2827, 12brcnv 5337 . . . . . . . . . . . . . . 15 (𝑥Domain𝑓𝑓Domain𝑥)
2912, 27brdomain 32165 . . . . . . . . . . . . . . 15 (𝑓Domain𝑥𝑥 = dom 𝑓)
3028, 29bitri 264 . . . . . . . . . . . . . 14 (𝑥Domain𝑓𝑥 = dom 𝑓)
3130anbi1i 731 . . . . . . . . . . . . 13 ((𝑥Domain𝑓𝑥 ∈ On) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3226, 31bitri 264 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3332exbii 1814 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On))
3413, 14ceqsexv 3273 . . . . . . . . . . 11 (∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
3533, 34bitri 264 . . . . . . . . . 10 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ dom 𝑓 ∈ On)
3624, 25, 353bitri 286 . . . . . . . . 9 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
3723, 36anbi12i 733 . . . . . . . 8 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3822, 37bitri 264 . . . . . . 7 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3938anbi1i 731 . . . . . 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 4738 . . . . . . . . . . . . . . 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 3234 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4212, 41brco 5325 . . . . . . . . . . . . . . . . 17 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
4329anbi1i 731 . . . . . . . . . . . . . . . . . . 19 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
4443exbii 1814 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
45 breq1 4688 . . . . . . . . . . . . . . . . . . 19 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
4613, 45ceqsexv 3273 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4744, 46bitri 264 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4813, 41brcnv 5337 . . . . . . . . . . . . . . . . . 18 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
4913epelc 5060 . . . . . . . . . . . . . . . . . 18 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
5048, 49bitri 264 . . . . . . . . . . . . . . . . 17 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
5142, 47, 503bitri 286 . . . . . . . . . . . . . . . 16 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
5251anbi1i 731 . . . . . . . . . . . . . . 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 5786 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
55543adant1 1099 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
56 brun 4736 . . . . . . . . . . . . . . . . . . . . . . . . 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 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}))
58 opelxp 5180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
5912, 58mpbiran 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
60 velsn 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
6159, 60bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
62 velsn 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ { {𝐴}} ↔ 𝑥 = {𝐴})
6361, 62anbi12i 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
6457, 63bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
65 brun 4736 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × Limits )))
67 opex 4962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑓, 𝑦⟩ ∈ V
6867, 27brco 5325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥))
69 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑧 ∈ V
7012, 41, 69brimg 32169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩Img𝑧𝑧 = (𝑓𝑦))
7127brbigcup 32130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 Bigcup 𝑥 𝑧 = 𝑥)
7270, 71anbi12i 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7372exbii 1814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
74 imaexg 7145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 ∈ V → (𝑓𝑦) ∈ V)
7512, 74ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓𝑦) ∈ V
76 unieq 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑦) → 𝑧 = (𝑓𝑦))
7776eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑦) → ( 𝑧 = 𝑥 (𝑓𝑦) = 𝑥))
7875, 77ceqsexv 3273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ (𝑓𝑦) = 𝑥)
79 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑦) = 𝑥𝑥 = (𝑓𝑦))
8078, 79bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ 𝑥 = (𝑓𝑦))
8168, 73, 803bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥𝑥 = (𝑓𝑦))
82 opelxp 5180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 Limits ))
8312, 82mpbiran 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 Limits )
8441ellimits 32142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 Limits ↔ Lim 𝑦)
8583, 84bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
8681, 85anbi12ci 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × Limits )) ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8766, 86bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8827brres 5437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ∧ ⟨𝑓, 𝑦⟩ ∈ (V × ran Succ)))
8967, 27brco 5325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥))
90 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑎 ∈ V
9167, 90brco 5325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎))
9212, 41, 69brpprod3a 32118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏))
93 3anrot 1060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩))
9490ideq 5307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 I 𝑎𝑓 = 𝑎)
95 equcom 1991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 = 𝑎𝑎 = 𝑓)
9694, 95bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑓 I 𝑎𝑎 = 𝑓)
97 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 𝑏 ∈ V
9897brbigcup 32130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 Bigcup 𝑏 𝑦 = 𝑏)
99 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ( 𝑦 = 𝑏𝑏 = 𝑦)
10098, 99bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 Bigcup 𝑏𝑏 = 𝑦)
101 biid 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
10296, 100, 1013anbi123i 1270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
10393, 102bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
1041032exbii 1815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
105 vuniex 6996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑦 ∈ V
106 opeq1 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
107106eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
108 opeq2 4434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑏 = 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, 𝑦⟩)
109108eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑦⟩))
11012, 105, 107, 109ceqsex2v 3276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, 𝑦⟩)
11192, 104, 1103bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧 = ⟨𝑓, 𝑦⟩)
112111anbi1i 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
113112exbii 1814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
114 opex 4962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑓, 𝑦⟩ ∈ V
115 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ⟨𝑓, 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, 𝑦⟩Apply𝑎))
116114, 115ceqsexv 3273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, 𝑦⟩Apply𝑎)
11712, 105, 90brapply 32170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟨𝑓, 𝑦⟩Apply𝑎𝑎 = (𝑓 𝑦))
118116, 117bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓 𝑦))
11991, 113, 1183bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎 = (𝑓 𝑦))
12090, 27brfullfun 32180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎FullFun𝐹𝑥𝑥 = (𝐹𝑎))
121119, 120anbi12i 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
122121exbii 1814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
123 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 𝑦) ∈ V
124 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = (𝑓 𝑦) → (𝐹𝑎) = (𝐹‘(𝑓 𝑦)))
125124eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = (𝑓 𝑦) → (𝑥 = (𝐹𝑎) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
126123, 125ceqsexv 3273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)) ↔ 𝑥 = (𝐹‘(𝑓 𝑦)))
12789, 122, 1263bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥𝑥 = (𝐹‘(𝑓 𝑦)))
128 opelxp 5180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
12912, 128mpbiran 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
13041elrn 5398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
13169, 41brsuccf 32173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧Succ𝑦𝑦 = suc 𝑧)
132131exbii 1814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
133129, 130, 1323bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
134127, 133anbi12ci 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 542 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 542 . . . . . . . . . . . . . . . . . . . . . . . . 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 7088 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
141 nlim0 5821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim ∅
142 limeq 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
143141, 142mtbiri 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ Lim 𝑦)
144143intnanrd 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
145 nsuceq0 5843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 suc 𝑧 ≠ ∅
146 neeq2 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = ∅ → (suc 𝑧𝑦 ↔ suc 𝑧 ≠ ∅))
147145, 146mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = ∅ → suc 𝑧𝑦)
148147necomd 2878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
149148neneqd 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
150149nexdv 1904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
151150intnanrd 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
152 ioran 510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) ↔ (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
153144, 151, 152sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → ¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
154 orel2 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
155153, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
156 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
157 unisnif 32157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
158156, 157syl6eqr 2703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = {𝐴})
159158eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = {𝐴}))
160159biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
161160adantld 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
169145, 168mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧𝑦 ≠ ∅)
170169neneqd 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
171170intnanrd 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
172171rexlimivw 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
173 orel1 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
174172, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
175 nlimsucg 7084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ V → ¬ Lim suc 𝑧)
17669, 175ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim suc 𝑧
177 limeq 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
178176, 177mtbiri 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
179178rexlimivw 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
180179intnanrd 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
181 orel1 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
182180, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
183145neii 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ¬ suc 𝑧 = ∅
184183iffalsei 4129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))
185 iffalse 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧)))
18669, 175, 185mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧))
187184, 186eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = (𝐹‘(𝑓 suc 𝑧))
188 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
189 unieq 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = suc 𝑧 𝑦 = suc 𝑧)
190189fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = suc 𝑧 → (𝑓 𝑦) = (𝑓 suc 𝑧))
191190fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = suc 𝑧 → (𝐹‘(𝑓 𝑦)) = (𝐹‘(𝑓 suc 𝑧)))
192177, 191ifbieq2d 4144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))
193188, 192ifbieq2d 4144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
194187, 193, 1913eqtr4a 2711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
195194rexlimivw 3058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
196195eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
197196biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
198197adantld 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
201196biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝐹‘(𝑓 𝑦))))
202 olc 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
203202olcd 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
208207, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
209178exlimiv 1898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
210209con2i 134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
211210intnanrd 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
212 orel2 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
213211, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
214206iffalsed 4130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
215 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = (𝑓𝑦))
216214, 215eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝑓𝑦))
217216eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝑓𝑦)))
218217biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = (𝑓𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
219218adantld 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → ((Lim 𝑦𝑥 = (𝑓𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
220208, 213, 2193syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
221220adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
225224olcd 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
226223, 225syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
227226adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1431 . . . . . . . . . . . . . . . . . . . . . . . . 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 5337 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
23412, 41, 27brapply 32170 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
235233, 234bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦)))
237232, 236anbi12d 747 . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . 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 1890 . . . . . . . . . . . . . . . . . . 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 4686 . . . . . . . . . . . . . . . . . . . 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 32135 . . . . . . . . . . . . . . . . . . . 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 5325 . . . . . . . . . . . . . . . . . . . 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 6239 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
246245eqvinc 3361 . . . . . . . . . . . . . . . . . . 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 307 . . . . . . . . . . . . . . . . 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 1286 . . . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . . . 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 1890 . . . . . . . . . . . 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 1794 . . . . . . . . . . . 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 5353 . . . . . . . . . . 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 344 . . . . . . . . 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 2946 . . . . . . . . 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 670 . . . . . . 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 682 . . . . . . 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 2767 . . 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 4477 . 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 2676 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 382  wa 383  w3o 1053  w3a 1054  wal 1521   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cun 3605  cin 3606  c0 3948  ifcif 4119  {csn 4210  cop 4216   cuni 4468   class class class wbr 4685   I cid 5052   E cep 5057   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147  Oncon0 5761  Lim wlim 5762  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  cfv 5926  reccrdg 7550  pprodcpprod 32063   Bigcup cbigcup 32066   Fix cfix 32067   Limits climits 32068   Funs cfuns 32069  Imgcimg 32074  Domaincdomain 32075  Applycapply 32077  Succcsuccf 32080  FullFuncfullfn 32082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-symdif 3877  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-txp 32086  df-pprod 32087  df-bigcup 32090  df-fix 32091  df-limits 32092  df-funs 32093  df-singleton 32094  df-singles 32095  df-image 32096  df-cart 32097  df-img 32098  df-domain 32099  df-cup 32101  df-succf 32104  df-apply 32105  df-funpart 32106  df-fullfun 32107
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator