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 32523
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 32166 . 2 rec(𝐹, 𝐴) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
2 an12 635 . . . . . . . 8 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
3 df-fn 6073 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4 ancom 452 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5 eqcom 2772 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
65anbi1i 617 . . . . . . . . . 10 ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
73, 4, 63bitri 288 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
87anbi1i 617 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
9 anass 460 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
102, 8, 93bitri 288 . . . . . . 7 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1110exbii 1943 . . . . . 6 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
12 vex 3353 . . . . . . . 8 𝑓 ∈ V
1312dmex 7301 . . . . . . 7 dom 𝑓 ∈ V
14 eleq1 2832 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15 raleq 3286 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
1614, 15anbi12d 624 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1716anbi2d 622 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))))
1813, 17ceqsexv 3395 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
1911, 18bitri 266 . . . . 5 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
20 df-rex 3061 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
21 eldif 3744 . . . . . 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 3960 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
2312elfuns 32487 . . . . . . . . 9 (𝑓 Funs ↔ Fun 𝑓)
2412elima 5655 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
25 df-rex 3061 . . . . . . . . . 10 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓))
26 vex 3353 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2726, 12brcnv 5475 . . . . . . . . . . . . . 14 (𝑥Domain𝑓𝑓Domain𝑥)
2812, 26brdomain 32505 . . . . . . . . . . . . . 14 (𝑓Domain𝑥𝑥 = dom 𝑓)
2927, 28bitri 266 . . . . . . . . . . . . 13 (𝑥Domain𝑓𝑥 = dom 𝑓)
3029anbi1ci 619 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ (𝑥 = dom 𝑓𝑥 ∈ On))
3130exbii 1943 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On))
3213, 14ceqsexv 3395 . . . . . . . . . . 11 (∃𝑥(𝑥 = dom 𝑓𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
3331, 32bitri 266 . . . . . . . . . 10 (∃𝑥(𝑥 ∈ On ∧ 𝑥Domain𝑓) ↔ dom 𝑓 ∈ On)
3424, 25, 333bitri 288 . . . . . . . . 9 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
3523, 34anbi12i 620 . . . . . . . 8 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3622, 35bitri 266 . . . . . . 7 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3736anbi1i 617 . . . . . 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 4864 . . . . . . . . . . . . . . 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 3353 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4012, 39brco 5463 . . . . . . . . . . . . . . . . 17 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
4128anbi1i 617 . . . . . . . . . . . . . . . . . . 19 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
4241exbii 1943 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
43 breq1 4814 . . . . . . . . . . . . . . . . . . 19 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
4413, 43ceqsexv 3395 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4542, 44bitri 266 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
4613, 39brcnv 5475 . . . . . . . . . . . . . . . . . 18 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
4713epeli 5194 . . . . . . . . . . . . . . . . . 18 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
4846, 47bitri 266 . . . . . . . . . . . . . . . . 17 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
4940, 45, 483bitri 288 . . . . . . . . . . . . . . . 16 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
5049anbi1i 617 . . . . . . . . . . . . . . 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 266 . . . . . . . . . . . . . 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 5935 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53523adant1 1160 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54 brun 4862 . . . . . . . . . . . . . . . . . . . . . . . . 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 5325 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}))
56 opelxp 5315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
5712, 56mpbiran 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58 velsn 4352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
5957, 58bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60 velsn 4352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ { {𝐴}} ↔ 𝑥 = {𝐴})
6159, 60anbi12i 620 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ { {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
6255, 61bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
63 brun 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65 opelxp 5315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 Limits ))
6612, 65mpbiran 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 Limits )
6739ellimits 32482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 Limits ↔ Lim 𝑦)
6866, 67bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69 opex 5090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑓, 𝑦⟩ ∈ V
7069, 26brco 5463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥))
71 vex 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑧 ∈ V
7212, 39, 71brimg 32509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩Img𝑧𝑧 = (𝑓𝑦))
7326brbigcup 32470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 Bigcup 𝑥 𝑧 = 𝑥)
7472, 73anbi12i 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7574exbii 1943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥))
7612imaex 7306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓𝑦) ∈ V
77 unieq 4604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑦) → 𝑧 = (𝑓𝑦))
7877eqeq1d 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑦) → ( 𝑧 = 𝑥 (𝑓𝑦) = 𝑥))
7976, 78ceqsexv 3395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ (𝑓𝑦) = 𝑥)
80 eqcom 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑦) = 𝑥𝑥 = (𝑓𝑦))
8179, 80bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(𝑧 = (𝑓𝑦) ∧ 𝑧 = 𝑥) ↔ 𝑥 = (𝑓𝑦))
8270, 75, 813bitri 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥𝑥 = (𝑓𝑦))
8368, 82anbi12i 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8464, 83bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦𝑥 = (𝑓𝑦)))
8526brresi 5576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86 opelxp 5315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
8712, 86mpbiran 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
8839elrn 5537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
8971, 39brsuccf 32513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧Succ𝑦𝑦 = suc 𝑧)
9089exbii 1943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
9187, 88, 903bitri 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
9269, 26brco 5463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥))
93 vex 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑎 ∈ V
9469, 93brco 5463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎))
9512, 39, 71brpprod3a 32458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏))
96 3anrot 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩))
9793ideq 5445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 I 𝑎𝑓 = 𝑎)
98 equcom 2115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 = 𝑎𝑎 = 𝑓)
9997, 98bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑓 I 𝑎𝑎 = 𝑓)
100 vex 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 𝑏 ∈ V
101100brbigcup 32470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 Bigcup 𝑏 𝑦 = 𝑏)
102 eqcom 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ( 𝑦 = 𝑏𝑏 = 𝑦)
103101, 102bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 Bigcup 𝑏𝑏 = 𝑦)
104 biid 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
10599, 103, 1043anbi123i 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓 I 𝑎𝑦 Bigcup 𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
10696, 105bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
1071062exbii 1944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎𝑦 Bigcup 𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩))
108 vuniex 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑦 ∈ V
109 opeq1 4561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110109eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111 opeq2 4562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑏 = 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, 𝑦⟩)
112111eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑦⟩))
11312, 108, 110, 112ceqsex2v 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎𝑏(𝑎 = 𝑓𝑏 = 𝑦𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, 𝑦⟩)
11495, 107, 1133bitri 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧 = ⟨𝑓, 𝑦⟩)
115114anbi1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
116115exbii 1943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎))
117 opex 5090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑓, 𝑦⟩ ∈ V
118 breq1 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ⟨𝑓, 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, 𝑦⟩Apply𝑎))
119117, 118ceqsexv 3395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, 𝑦⟩Apply𝑎)
12012, 108, 93brapply 32510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟨𝑓, 𝑦⟩Apply𝑎𝑎 = (𝑓 𝑦))
121119, 120bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(𝑧 = ⟨𝑓, 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓 𝑦))
12294, 116, 1213bitri 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎 = (𝑓 𝑦))
12393, 26brfullfun 32520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎FullFun𝐹𝑥𝑥 = (𝐹𝑎))
124122, 123anbi12i 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
125124exbii 1943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)))
126 fvex 6392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 𝑦) ∈ V
127 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = (𝑓 𝑦) → (𝐹𝑎) = (𝐹‘(𝑓 𝑦)))
128127eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = (𝑓 𝑦) → (𝑥 = (𝐹𝑎) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
129126, 128ceqsexv 3395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(𝑎 = (𝑓 𝑦) ∧ 𝑥 = (𝐹𝑎)) ↔ 𝑥 = (𝐹‘(𝑓 𝑦)))
13092, 125, 1293bitri 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥𝑥 = (𝐹‘(𝑓 𝑦)))
13191, 130anbi12i 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥) ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13285, 131bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
13384, 132orbi12i 938 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13463, 133bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
13562, 134orbi12i 938 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑓, 𝑦⟩((V × {∅}) × { {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥) ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
13654, 135bitri 266 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩(((V × {∅}) × { {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
137 onzsl 7248 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138 nlim0 5968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim ∅
139 limeq 5922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140138, 139mtbiri 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ Lim 𝑦)
141140intnanrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
142 nsuceq0 5990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 suc 𝑧 ≠ ∅
143 neeq2 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = ∅ → (suc 𝑧𝑦 ↔ suc 𝑧 ≠ ∅))
144142, 143mpbiri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = ∅ → suc 𝑧𝑦)
145144necomd 2992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146145neneqd 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147146nexdv 2031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148147intnanrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
149 ioran 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) ↔ (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
150141, 148, 149sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → ¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
151 orel2 914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
153 iftrue 4251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154 unisnif 32497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155153, 154syl6eqr 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = {𝐴})
156155eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = {𝐴}))
157156biimprd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
158157adantld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
159152, 158syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
160156biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = {𝐴}))
161160anc2li 551 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = {𝐴})))
162 orc 893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
163161, 162syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
164159, 163impbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
165 neeq1 2999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166142, 165mpbiri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧𝑦 ≠ ∅)
167166neneqd 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168167intnanrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
169168rexlimivw 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
170 orel1 912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
172 nlimsucg 7244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ V → ¬ Lim suc 𝑧)
173172elv 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim suc 𝑧
174 limeq 5922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175173, 174mtbiri 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176175rexlimivw 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177176intnanrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦𝑥 = (𝑓𝑦)))
178 orel1 912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (Lim 𝑦𝑥 = (𝑓𝑦)) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
180142neii 2939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ¬ suc 𝑧 = ∅
181180iffalsei 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))
182 iffalse 4254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧)))
18371, 172, 182mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧))
184181, 183eqtri 2787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = (𝐹‘(𝑓 suc 𝑧))
185 eqeq1 2769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186 unieq 4604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = suc 𝑧 𝑦 = suc 𝑧)
187186fveq2d 6383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = suc 𝑧 → (𝑓 𝑦) = (𝑓 suc 𝑧))
188187fveq2d 6383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = suc 𝑧 → (𝐹‘(𝑓 𝑦)) = (𝐹‘(𝑓 suc 𝑧)))
189174, 188ifbieq2d 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))
190185, 189ifbieq2d 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
191184, 190, 1883eqtr4a 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
192191rexlimivw 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝐹‘(𝑓 𝑦)))
193192eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓 𝑦))))
194193biimprd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
195194adantld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198193biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝐹‘(𝑓 𝑦))))
199 olc 894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
200199olcd 900 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
201197, 198, 200syl6an 674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
202196, 201impbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
203140con2i 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ 𝑦 = ∅)
204203intnanrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = {𝐴}))
205204, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
206175exlimiv 2025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207206con2i 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208207intnanrd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))
209 orel2 914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))) → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
211203iffalsed 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
212 iftrue 4251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = (𝑓𝑦))
213211, 212eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = (𝑓𝑦))
214213eqeq2d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ 𝑥 = (𝑓𝑦)))
215214biimprd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = (𝑓𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
216215adantld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → ((Lim 𝑦𝑥 = (𝑓𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
217205, 210, 2163syld 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
218217adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
219214biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → 𝑥 = (𝑓𝑦)))
220219anc2li 551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → (Lim 𝑦𝑥 = (𝑓𝑦))))
221 orc 893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))
222221olcd 900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Lim 𝑦𝑥 = (𝑓𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))))
223220, 222syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
224223adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦)))))))
225218, 224impbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
226164, 202, 2253jaoi 1552 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
227137, 226sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = {𝐴}) ∨ ((Lim 𝑦𝑥 = (𝑓𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧𝑥 = (𝐹‘(𝑓 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
228136, 227syl5bb 274 . . . . . . . . . . . . . . . . . . . . . . 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 5475 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
23112, 39, 26brapply 32510 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
232230, 231bitri 266 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦)))
234229, 233anbi12d 624 . . . . . . . . . . . . . . . . . . . . 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 455 . . . . . . . . . . . . . . . . . . . 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 2016 . . . . . . . . . . . . . . . . . . 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 4812 . . . . . . . . . . . . . . . . . . . 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 32475 . . . . . . . . . . . . . . . . . . . 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 5463 . . . . . . . . . . . . . . . . . . . 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 288 . . . . . . . . . . . . . . . . . . 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 6392 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
242241eqvinc 3484 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
243236, 240, 2423bitr4g 305 . . . . . . . . . . . . . . . . . 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 309 . . . . . . . . . . . . . . . . 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 1150 . . . . . . . . . . . . . . . 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 572 . . . . . . . . . . . . . . 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 392 . . . . . . . . . . . . . . 15 ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
248246, 247syl6bb 278 . . . . . . . . . . . . . 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, 248syl5bb 274 . . . . . . . . . . . . 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 2016 . . . . . . . . . . . 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 1921 . . . . . . . . . . . 12 (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
252250, 251syl6rbb 279 . . . . . . . . . . 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 5491 . . . . . . . . . . 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, 253syl6bbr 280 . . . . . . . . . 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 346 . . . . . . . . 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 3060 . . . . . . . . 9 (∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
257255, 256syl6bbr 280 . . . . . . . 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 570 . . . . . . 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 460 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
260258, 259bitri 266 . . . . . 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 288 . . . . 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 295 . . . 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 2881 . . 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 4605 . 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 2790 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 197  wa 384  wo 873  w3o 1106  w3a 1107  wal 1650   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  wral 3055  wrex 3056  Vcvv 3350  cdif 3731  cun 3732  cin 3733  c0 4081  ifcif 4245  {csn 4336  cop 4342   cuni 4596   class class class wbr 4811   I cid 5186   E cep 5191   × cxp 5277  ccnv 5278  dom cdm 5279  ran crn 5280  cres 5281  cima 5282  ccom 5283  Oncon0 5910  Lim wlim 5911  suc csuc 5912  Fun wfun 6064   Fn wfn 6065  cfv 6070  reccrdg 7713  pprodcpprod 32403   Bigcup cbigcup 32406   Fix cfix 32407   Limits climits 32408   Funs cfuns 32409  Imgcimg 32414  Domaincdomain 32415  Applycapply 32417  Succcsuccf 32420  FullFuncfullfn 32422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-symdif 4007  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-txp 32426  df-pprod 32427  df-bigcup 32430  df-fix 32431  df-limits 32432  df-funs 32433  df-singleton 32434  df-singles 32435  df-image 32436  df-cart 32437  df-img 32438  df-domain 32439  df-cup 32441  df-succf 32444  df-apply 32445  df-funpart 32446  df-fullfun 32447
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator