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 35932
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 35777 . 2 rec(𝐹, 𝐴) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2 an12 645 . . . . . . . 8 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
3 df-fn 6565 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4 ancom 460 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5 eqcom 2741 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
65anbi1i 624 . . . . . . . . . 10 ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
73, 4, 63bitri 297 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
87anbi1i 624 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
9 anass 468 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
102, 8, 93bitri 297 . . . . . . 7 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1110exbii 1844 . . . . . 6 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
12 vex 3481 . . . . . . . 8 𝑓 ∈ V
1312dmex 7931 . . . . . . 7 dom 𝑓 ∈ V
14 eleq1 2826 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15 raleq 3320 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
1614, 15anbi12d 632 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1716anbi2d 630 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1813, 17ceqsexv 3529 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1911, 18bitri 275 . . . . 5 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
20 df-rex 3068 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
21 eldif 3972 . . . . . 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 3978 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
2312elfuns 35896 . . . . . . . . 9 (𝑓 Funs ↔ Fun 𝑓)
2412elima 6084 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
25 df-rex 3068 . . . . . . . . . 10 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓))
26 vex 3481 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2726, 12brcnv 5895 . . . . . . . . . . . . . 14 (𝑥Domain𝑓𝑓Domain𝑥)
2812, 26brdomain 35914 . . . . . . . . . . . . . 14 (𝑓Domain𝑥𝑥 = dom 𝑓)
2927, 28bitri 275 . . . . . . . . . . . . 13 (𝑥Domain𝑓𝑥 = dom 𝑓)
3029anbi1ci 626 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3130exbii 1844 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On))
3213, 14ceqsexv 3529 . . . . . . . . . . 11 (∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
3331, 32bitri 275 . . . . . . . . . 10 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ dom 𝑓 ∈ On)
3424, 25, 333bitri 297 . . . . . . . . 9 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
3523, 34anbi12i 628 . . . . . . . 8 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3622, 35bitri 275 . . . . . . 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 5200 . . . . . . . . . . . . . . 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 3481 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4012, 39brco 5883 . . . . . . . . . . . . . . . . 17 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
4128anbi1i 624 . . . . . . . . . . . . . . . . . . 19 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
4241exbii 1844 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
43 breq1 5150 . . . . . . . . . . . . . . . . . . 19 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
4413, 43ceqsexv 3529 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4542, 44bitri 275 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4613, 39brcnv 5895 . . . . . . . . . . . . . . . . . 18 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
4713epeli 5590 . . . . . . . . . . . . . . . . . 18 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
4846, 47bitri 275 . . . . . . . . . . . . . . . . 17 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
4940, 45, 483bitri 297 . . . . . . . . . . . . . . . 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 275 . . . . . . . . . . . . . 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 6410 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53523adant1 1129 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54 brun 5198 . . . . . . . . . . . . . . . . . . . . . . . . 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 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}))
56 opelxp 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
5712, 56mpbiran 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58 velsn 4646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
5957, 58bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60 velsn 4646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ { {𝐴}} ↔ 𝑥 = {𝐴})
6159, 60anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
6255, 61bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
63 brun 5198 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65 opelxp 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 Limits ))
6612, 65mpbiran 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 Limits )
6739ellimits 35891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 Limits ↔ Lim 𝑦)
6866, 67bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69 opex 5474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑓, 𝑦⟩ ∈ V
7069, 26brco 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥))
71 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑧 ∈ V
7212, 39, 71brimg 35918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩Img𝑧𝑧 = (𝑓𝑦))
7326brbigcup 35879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 Bigcup 𝑥 𝑧 = 𝑥)
7472, 73anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7574exbii 1844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7612imaex 7936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓𝑦) ∈ V
77 unieq 4922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑦) → 𝑧 = (𝑓𝑦))
7877eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑦) → ( 𝑧 = 𝑥 (𝑓𝑦) = 𝑥))
7976, 78ceqsexv 3529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ (𝑓𝑦) = 𝑥)
80 eqcom 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑦) = 𝑥𝑥 = (𝑓𝑦))
8179, 80bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ 𝑥 = (𝑓𝑦))
8270, 75, 813bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥𝑥 = (𝑓𝑦))
8368, 82anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8464, 83bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8526brresi 6008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86 opelxp 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
8712, 86mpbiran 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
8839elrn 5906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
8971, 39brsuccf 35922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧Succ𝑦𝑦 = suc 𝑧)
9089exbii 1844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
9187, 88, 903bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
9269, 26brco 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥))
93 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑎 ∈ V
9469, 93brco 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎))
9512, 39, 71brpprod3a 35867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏))
96 3anrot 1099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩))
9793ideq 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 I 𝑎𝑓 = 𝑎)
98 equcom 2014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 = 𝑎𝑎 = 𝑓)
9997, 98bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑓 I 𝑎𝑎 = 𝑓)
100 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 𝑏 ∈ V
101100brbigcup 35879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 Bigcup 𝑏 𝑦 = 𝑏)
102 eqcom 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ( 𝑦 = 𝑏𝑏 = 𝑦)
103101, 102bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 Bigcup 𝑏𝑏 = 𝑦)
104 biid 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
10599, 103, 1043anbi123i 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
10696, 105bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
1071062exbii 1845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
108 vuniex 7757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑦 ∈ V
109 opeq1 4877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110109eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111 opeq2 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑏 = 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, 𝑦⟩)
112111eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑦⟩))
11312, 108, 110, 112ceqsex2v 3535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, 𝑦⟩)
11495, 107, 1133bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧 = ⟨𝑓, 𝑦⟩)
115114anbi1i 624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
116115exbii 1844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
117 opex 5474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑓, 𝑦⟩ ∈ V
118 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ⟨𝑓, 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, 𝑦⟩Apply𝑎))
119117, 118ceqsexv 3529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, 𝑦⟩Apply𝑎)
12012, 108, 93brapply 35919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟨𝑓, 𝑦⟩Apply𝑎𝑎 = (𝑓 𝑦))
121119, 120bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓 𝑦))
12294, 116, 1213bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎 = (𝑓 𝑦))
12393, 26brfullfun 35929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎FullFun𝐹𝑥𝑥 = (𝐹𝑎))
124122, 123anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
125124exbii 1844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
126 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 𝑦) ∈ V
127 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = (𝑓 𝑦) → (𝐹𝑎) = (𝐹‘(𝑓 𝑦)))
128127eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = (𝑓 𝑦) → (𝑥 = (𝐹𝑎) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
129126, 128ceqsexv 3529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)) ↔ 𝑥 = (𝐹‘(𝑓 𝑦)))
13092, 125, 1293bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥𝑥 = (𝐹‘(𝑓 𝑦)))
13191, 130anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥) ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13285, 131bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13384, 132orbi12i 914 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13463, 133bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13562, 134orbi12i 914 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥) ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
13654, 135bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
137 onzsl 7866 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138 nlim0 6444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim ∅
139 limeq 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140138, 139mtbiri 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ Lim 𝑦)
141140intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
142 nsuceq0 6468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 suc 𝑧 ≠ ∅
143 neeq2 3001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = ∅ → (suc 𝑧𝑦 ↔ suc 𝑧 ≠ ∅))
144142, 143mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = ∅ → suc 𝑧𝑦)
145144necomd 2993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146145neneqd 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147146nexdv 1933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148147intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
149 ioran 985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) ↔ (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
150141, 148, 149sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → ¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
151 orel2 890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
153 iftrue 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154 unisnif 35906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155153, 154eqtr4di 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = {𝐴})
156155eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = {𝐴}))
157156biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
158157adantld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
159152, 158syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
160156biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = {𝐴}))
161160anc2li 555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
162 orc 867 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
163161, 162syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
164159, 163impbid 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
165 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166142, 165mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧𝑦 ≠ ∅)
167166neneqd 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168167intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
169168rexlimivw 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
170 orel1 888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
172 nlimsucg 7862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ V → ¬ Lim suc 𝑧)
173172elv 3482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim suc 𝑧
174 limeq 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175173, 174mtbiri 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176175rexlimivw 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177176intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
178 orel1 888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
180142neii 2939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ¬ suc 𝑧 = ∅
181180iffalsei 4540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))
182 iffalse 4539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧)))
18371, 172, 182mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧))
184181, 183eqtri 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = (𝐹‘(𝑓 suc 𝑧))
185 eqeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186 unieq 4922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = suc 𝑧 𝑦 = suc 𝑧)
187186fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = suc 𝑧 → (𝑓 𝑦) = (𝑓 suc 𝑧))
188187fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = suc 𝑧 → (𝐹‘(𝑓 𝑦)) = (𝐹‘(𝑓 suc 𝑧)))
189174, 188ifbieq2d 4556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))
190185, 189ifbieq2d 4556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
191184, 190, 1883eqtr4a 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
192191rexlimivw 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
193192eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
194193biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
195194adantld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198193biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝐹‘(𝑓 𝑦))))
199 olc 868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
200199olcd 874 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
201197, 198, 200syl6an 684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
202196, 201impbid 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
203140con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ 𝑦 = ∅)
204203intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
205204, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
206175exlimiv 1927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207206con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208207intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
209 orel2 890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
211203iffalsed 4541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
212 iftrue 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = (𝑓𝑦))
213211, 212eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝑓𝑦))
214213eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝑓𝑦)))
215214biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = (𝑓𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
216215adantld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → ((Lim 𝑦𝑥 = (𝑓𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
217205, 210, 2163syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
218217adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
219214biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝑓𝑦)))
220219anc2li 555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
221 orc 867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
222221olcd 874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
223220, 222syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
224223adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
225218, 224impbid 212 . . . . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
228136, 227bitrid 283 . . . . . . . . . . . . . . . . . . . . . . 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 5895 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
23112, 39, 26brapply 35919 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
232230, 231bitri 275 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦)))
234229, 233anbi12d 632 . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . 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 1918 . . . . . . . . . . . . . . . . . . 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 5148 . . . . . . . . . . . . . . . . . . . 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 35884 . . . . . . . . . . . . . . . . . . . 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 5883 . . . . . . . . . . . . . . . . . . . 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 297 . . . . . . . . . . . . . . . . . . 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 6919 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
242241eqvinc 3648 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
243236, 240, 2423bitr4g 314 . . . . . . . . . . . . . . . . . 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 318 . . . . . . . . . . . . . . . . 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 1120 . . . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . . . 15 ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
248246, 247bitrdi 287 . . . . . . . . . . . . . 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 283 . . . . . . . . . . . . 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 1918 . . . . . . . . . . . 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 1823 . . . . . . . . . . . 12 (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
252250, 251bitr2di 288 . . . . . . . . . . 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 5913 . . . . . . . . . . 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 289 . . . . . . . . . 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 3059 . . . . . . . . 9 (∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
257255, 256bitr4di 289 . . . . . . . 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 574 . . . . . . 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 468 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
260258, 259bitri 275 . . . . . 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 297 . . . . 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 304 . . . 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 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
263262eqabi 2874 . . 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 4923 . 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 2765 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 206  wa 395  wo 847  w3o 1085  w3a 1086  wal 1534   = wceq 1536  wex 1775  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  cin 3961  c0 4338  ifcif 4530  {csn 4630  cop 4636   cuni 4911   class class class wbr 5147   I cid 5581   E cep 5587   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  ccom 5692  Oncon0 6385  Lim wlim 6386  suc csuc 6387  Fun wfun 6556   Fn wfn 6557  cfv 6562  reccrdg 8447  pprodcpprod 35812   Bigcup cbigcup 35815   Fix cfix 35816   Limits climits 35817   Funs cfuns 35818  Imgcimg 35823  Domaincdomain 35824  Applycapply 35826  Succcsuccf 35829  FullFuncfullfn 35831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-symdif 4258  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-txp 35835  df-pprod 35836  df-bigcup 35839  df-fix 35840  df-limits 35841  df-funs 35842  df-singleton 35843  df-singles 35844  df-image 35845  df-cart 35846  df-img 35847  df-domain 35848  df-cup 35850  df-succf 35853  df-apply 35854  df-funpart 35855  df-fullfun 35856
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator