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 34536
Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
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 34371 . 2 rec(𝐹, 𝐴) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2 an12 643 . . . . . . . 8 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
3 df-fn 6499 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4 ancom 461 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5 eqcom 2743 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
65anbi1i 624 . . . . . . . . . 10 ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
73, 4, 63bitri 296 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
87anbi1i 624 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
9 anass 469 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
102, 8, 93bitri 296 . . . . . . 7 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1110exbii 1850 . . . . . 6 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
12 vex 3449 . . . . . . . 8 𝑓 ∈ V
1312dmex 7848 . . . . . . 7 dom 𝑓 ∈ V
14 eleq1 2825 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15 raleq 3309 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
1614, 15anbi12d 631 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1716anbi2d 629 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1813, 17ceqsexv 3494 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1911, 18bitri 274 . . . . 5 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
20 df-rex 3074 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
21 eldif 3920 . . . . . 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 3926 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
2312elfuns 34500 . . . . . . . . 9 (𝑓 Funs ↔ Fun 𝑓)
2412elima 6018 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
25 df-rex 3074 . . . . . . . . . 10 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓))
26 vex 3449 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2726, 12brcnv 5838 . . . . . . . . . . . . . 14 (𝑥Domain𝑓𝑓Domain𝑥)
2812, 26brdomain 34518 . . . . . . . . . . . . . 14 (𝑓Domain𝑥𝑥 = dom 𝑓)
2927, 28bitri 274 . . . . . . . . . . . . 13 (𝑥Domain𝑓𝑥 = dom 𝑓)
3029anbi1ci 626 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3130exbii 1850 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On))
3213, 14ceqsexv 3494 . . . . . . . . . . 11 (∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
3331, 32bitri 274 . . . . . . . . . 10 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ dom 𝑓 ∈ On)
3424, 25, 333bitri 296 . . . . . . . . 9 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
3523, 34anbi12i 627 . . . . . . . 8 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3622, 35bitri 274 . . . . . . 7 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3736anbi1i 624 . . . . . 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))))))))
38 brdif 5158 . . . . . . . . . . . . . . 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)))))𝑦))
39 vex 3449 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4012, 39brco 5826 . . . . . . . . . . . . . . . . 17 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
4128anbi1i 624 . . . . . . . . . . . . . . . . . . 19 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
4241exbii 1850 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
43 breq1 5108 . . . . . . . . . . . . . . . . . . 19 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
4413, 43ceqsexv 3494 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4542, 44bitri 274 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4613, 39brcnv 5838 . . . . . . . . . . . . . . . . . 18 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
4713epeli 5539 . . . . . . . . . . . . . . . . . 18 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
4846, 47bitri 274 . . . . . . . . . . . . . . . . 17 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
4940, 45, 483bitri 296 . . . . . . . . . . . . . . . 16 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
5049anbi1i 624 . . . . . . . . . . . . . . 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)))))𝑦))
5138, 50bitri 274 . . . . . . . . . . . . . 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)))))𝑦))
52 onelon 6342 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53523adant1 1130 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54 brun 5156 . . . . . . . . . . . . . . . . . . . . . . . . 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)))𝑥))
55 brxp 5681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}))
56 opelxp 5669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
5712, 56mpbiran 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58 velsn 4602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
5957, 58bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60 velsn 4602 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ { {𝐴}} ↔ 𝑥 = {𝐴})
6159, 60anbi12i 627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
6255, 61bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
63 brun 5156 . . . . . . . . . . . . . . . . . . . . . . . . . . 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))𝑥))
6426brresi 5946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65 opelxp 5669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 Limits ))
6612, 65mpbiran 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 Limits )
6739ellimits 34495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 Limits ↔ Lim 𝑦)
6866, 67bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69 opex 5421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑓, 𝑦⟩ ∈ V
7069, 26brco 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥))
71 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑧 ∈ V
7212, 39, 71brimg 34522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩Img𝑧𝑧 = (𝑓𝑦))
7326brbigcup 34483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 Bigcup 𝑥 𝑧 = 𝑥)
7472, 73anbi12i 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7574exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7612imaex 7853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓𝑦) ∈ V
77 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑦) → 𝑧 = (𝑓𝑦))
7877eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑦) → ( 𝑧 = 𝑥 (𝑓𝑦) = 𝑥))
7976, 78ceqsexv 3494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ (𝑓𝑦) = 𝑥)
80 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑦) = 𝑥𝑥 = (𝑓𝑦))
8179, 80bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ 𝑥 = (𝑓𝑦))
8270, 75, 813bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥𝑥 = (𝑓𝑦))
8368, 82anbi12i 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8464, 83bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8526brresi 5946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86 opelxp 5669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
8712, 86mpbiran 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
8839elrn 5849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
8971, 39brsuccf 34526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧Succ𝑦𝑦 = suc 𝑧)
9089exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
9187, 88, 903bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
9269, 26brco 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥))
93 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑎 ∈ V
9469, 93brco 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎))
9512, 39, 71brpprod3a 34471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏))
96 3anrot 1100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩))
9793ideq 5808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 I 𝑎𝑓 = 𝑎)
98 equcom 2021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 = 𝑎𝑎 = 𝑓)
9997, 98bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑓 I 𝑎𝑎 = 𝑓)
100 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 𝑏 ∈ V
101100brbigcup 34483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 Bigcup 𝑏 𝑦 = 𝑏)
102 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ( 𝑦 = 𝑏𝑏 = 𝑦)
103101, 102bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 Bigcup 𝑏𝑏 = 𝑦)
104 biid 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
10599, 103, 1043anbi123i 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
10696, 105bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
1071062exbii 1851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
108 vuniex 7676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑦 ∈ V
109 opeq1 4830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110109eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111 opeq2 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑏 = 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, 𝑦⟩)
112111eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑦⟩))
11312, 108, 110, 112ceqsex2v 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, 𝑦⟩)
11495, 107, 1133bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧 = ⟨𝑓, 𝑦⟩)
115114anbi1i 624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
116115exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
117 opex 5421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑓, 𝑦⟩ ∈ V
118 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ⟨𝑓, 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, 𝑦⟩Apply𝑎))
119117, 118ceqsexv 3494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, 𝑦⟩Apply𝑎)
12012, 108, 93brapply 34523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟨𝑓, 𝑦⟩Apply𝑎𝑎 = (𝑓 𝑦))
121119, 120bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓 𝑦))
12294, 116, 1213bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎 = (𝑓 𝑦))
12393, 26brfullfun 34533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎FullFun𝐹𝑥𝑥 = (𝐹𝑎))
124122, 123anbi12i 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
125124exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
126 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 𝑦) ∈ V
127 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = (𝑓 𝑦) → (𝐹𝑎) = (𝐹‘(𝑓 𝑦)))
128127eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = (𝑓 𝑦) → (𝑥 = (𝐹𝑎) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
129126, 128ceqsexv 3494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)) ↔ 𝑥 = (𝐹‘(𝑓 𝑦)))
13092, 125, 1293bitri 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥𝑥 = (𝐹‘(𝑓 𝑦)))
13191, 130anbi12i 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥) ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13285, 131bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13384, 132orbi12i 913 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13463, 133bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13562, 134orbi12i 913 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥) ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
13654, 135bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
137 onzsl 7782 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138 nlim0 6376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim ∅
139 limeq 6329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140138, 139mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ Lim 𝑦)
141140intnanrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
142 nsuceq0 6400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 suc 𝑧 ≠ ∅
143 neeq2 3007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = ∅ → (suc 𝑧𝑦 ↔ suc 𝑧 ≠ ∅))
144142, 143mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = ∅ → suc 𝑧𝑦)
145144necomd 2999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146145neneqd 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147146nexdv 1939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148147intnanrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
149 ioran 982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) ↔ (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
150141, 148, 149sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → ¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
151 orel2 889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
153 iftrue 4492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154 unisnif 34510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155153, 154eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = {𝐴})
156155eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = {𝐴}))
157156biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
158157adantld 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
159152, 158syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
160156biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = {𝐴}))
161160anc2li 556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
162 orc 865 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
163161, 162syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
164159, 163impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
165 neeq1 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166142, 165mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧𝑦 ≠ ∅)
167166neneqd 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168167intnanrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
169168rexlimivw 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
170 orel1 887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
172 nlimsucg 7778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ V → ¬ Lim suc 𝑧)
173172elv 3451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim suc 𝑧
174 limeq 6329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175173, 174mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176175rexlimivw 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177176intnanrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
178 orel1 887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
180142neii 2945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ¬ suc 𝑧 = ∅
181180iffalsei 4496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))
182 iffalse 4495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧)))
18371, 172, 182mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧))
184181, 183eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = (𝐹‘(𝑓 suc 𝑧))
185 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = suc 𝑧 𝑦 = suc 𝑧)
187186fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = suc 𝑧 → (𝑓 𝑦) = (𝑓 suc 𝑧))
188187fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = suc 𝑧 → (𝐹‘(𝑓 𝑦)) = (𝐹‘(𝑓 suc 𝑧)))
189174, 188ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))
190185, 189ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
191184, 190, 1883eqtr4a 2802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
192191rexlimivw 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
193192eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
194193biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
195194adantld 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
196171, 179, 1953syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
197 rexex 3079 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198193biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝐹‘(𝑓 𝑦))))
199 olc 866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
200199olcd 872 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
201197, 198, 200syl6an 682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
202196, 201impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
203140con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ 𝑦 = ∅)
204203intnanrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
205204, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
206175exlimiv 1933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207206con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208207intnanrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
209 orel2 889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
211203iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
212 iftrue 4492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = (𝑓𝑦))
213211, 212eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝑓𝑦))
214213eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝑓𝑦)))
215214biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = (𝑓𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
216215adantld 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → ((Lim 𝑦𝑥 = (𝑓𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
217205, 210, 2163syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
218217adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
219214biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝑓𝑦)))
220219anc2li 556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
221 orc 865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
222221olcd 872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
223220, 222syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
224223adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
225218, 224impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
226164, 202, 2253jaoi 1427 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
227137, 226sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
228136, 227bitrid 282 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ On → (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
22953, 228syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
23026, 69brcnv 5838 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
23112, 39, 26brapply 34523 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
232230, 231bitri 274 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦)))
234229, 233anbi12d 631 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ∧ 𝑥 = (𝑓𝑦))))
235234biancomd 464 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
236235exbidv 1924 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
237 df-br 5106 . . . . . . . . . . . . . . . . . . . 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))))))
23869elfix 34488 . . . . . . . . . . . . . . . . . . . 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)))))⟨𝑓, 𝑦⟩)
23969, 69brco 5826 . . . . . . . . . . . . . . . . . . . 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⟨𝑓, 𝑦⟩))
240237, 238, 2393bitri 296 . . . . . . . . . . . . . . . . . . 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⟨𝑓, 𝑦⟩))
241 fvex 6855 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
242241eqvinc 3599 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
243236, 240, 2423bitr4g 313 . . . . . . . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
244243notbid 317 . . . . . . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
2452443expia 1121 . . . . . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
246245pm5.32d 577 . . . . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
247 annim 404 . . . . . . . . . . . . . . 15 ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
248246, 247bitrdi 286 . . . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
24951, 248bitrid 282 . . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
250249exbidv 1924 . . . . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
251 exnal 1829 . . . . . . . . . . . 12 (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
252250, 251bitr2di 287 . . . . . . . . . . 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))))))𝑦))
25312eldm 5856 . . . . . . . . . . 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))))))𝑦)
254252, 253bitr4di 288 . . . . . . . . . 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))))))))
255254con1bid 355 . . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
256 df-ral 3065 . . . . . . . . 9 (∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
257255, 256bitr4di 288 . . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
258257pm5.32i 575 . . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
259 anass 469 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
260258, 259bitri 274 . . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
26121, 37, 2603bitri 296 . . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
26219, 20, 2613bitr4ri 303 . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
263262abbi2i 2873 . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
264263unieqi 4878 . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2651, 264eqtr4i 2767 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 205  wa 396  wo 845  w3o 1086  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cdif 3907  cun 3908  cin 3909  c0 4282  ifcif 4486  {csn 4586  cop 4592   cuni 4865   class class class wbr 5105   I cid 5530   E cep 5536   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ccom 5637  Oncon0 6317  Lim wlim 6318  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  cfv 6496  reccrdg 8355  pprodcpprod 34416   Bigcup cbigcup 34419   Fix cfix 34420   Limits climits 34421   Funs cfuns 34422  Imgcimg 34427  Domaincdomain 34428  Applycapply 34430  Succcsuccf 34433  FullFuncfullfn 34435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-symdif 4202  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-txp 34439  df-pprod 34440  df-bigcup 34443  df-fix 34444  df-limits 34445  df-funs 34446  df-singleton 34447  df-singles 34448  df-image 34449  df-cart 34450  df-img 34451  df-domain 34452  df-cup 34454  df-succf 34457  df-apply 34458  df-funpart 34459  df-fullfun 34460
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator