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 36167
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 36010 . 2 rec(𝐹, 𝐴) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
2 an12 646 . . . . . . . 8 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
3 df-fn 6503 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4 ancom 460 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5 eqcom 2744 . . . . . . . . . . 11 (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
65anbi1i 625 . . . . . . . . . 10 ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
73, 4, 63bitri 297 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
87anbi1i 625 . . . . . . . 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 1850 . . . . . 6 (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
12 vex 3446 . . . . . . . 8 𝑓 ∈ V
1312dmex 7861 . . . . . . 7 dom 𝑓 ∈ V
14 eleq1 2825 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15 raleq 3295 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
1614, 15anbi12d 633 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
1716anbi2d 631 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
1813, 17ceqsexv 3492 . . . . . 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 3063 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
21 eldif 3913 . . . . . 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 3919 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)))
2312elfuns 36129 . . . . . . . . 9 (𝑓 ∈ Funs ↔ Fun 𝑓)
2412elima 6032 . . . . . . . . . 10 (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓)
25 df-rex 3063 . . . . . . . . . 10 (∃𝑥 ∈ On 𝑥◡Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓))
26 vex 3446 . . . . . . . . . . . . . . 15 𝑥 ∈ V
2726, 12brcnv 5839 . . . . . . . . . . . . . 14 (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥)
2812, 26brdomain 36147 . . . . . . . . . . . . . 14 (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
2927, 28bitri 275 . . . . . . . . . . . . 13 (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
3029anbi1ci 627 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
3130exbii 1850 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
3213, 14ceqsexv 3492 . . . . . . . . . . 11 (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
3331, 32bitri 275 . . . . . . . . . 10 (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ dom 𝑓 ∈ On)
3424, 25, 333bitri 297 . . . . . . . . 9 (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On)
3523, 34anbi12i 629 . . . . . . . 8 ((𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3622, 35bitri 275 . . . . . . 7 (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
3736anbi1i 625 . . . . . 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 5153 . . . . . . . . . . . . . . 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 3446 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4012, 39brco 5827 . . . . . . . . . . . . . . . . 17 (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦))
4128anbi1i 625 . . . . . . . . . . . . . . . . . . 19 ((𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
4241exbii 1850 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
43 breq1 5103 . . . . . . . . . . . . . . . . . . 19 (𝑥 = dom 𝑓 → (𝑥◡ E 𝑦 ↔ dom 𝑓◡ E 𝑦))
4413, 43ceqsexv 3492 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
4542, 44bitri 275 . . . . . . . . . . . . . . . . 17 (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
4613, 39brcnv 5839 . . . . . . . . . . . . . . . . . 18 (dom 𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
4713epeli 5534 . . . . . . . . . . . . . . . . . 18 (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓)
4846, 47bitri 275 . . . . . . . . . . . . . . . . 17 (dom 𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓)
4940, 45, 483bitri 297 . . . . . . . . . . . . . . . 16 (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓)
5049anbi1i 625 . . . . . . . . . . . . . . 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 6350 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53523adant1 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54 brun 5151 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥))
55 brxp 5681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}))
56 opelxp 5668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
5712, 56mpbiran 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58 velsn 4598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
5957, 58bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60 velsn 4598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ {∪ {𝐴}} ↔ 𝑥 = ∪ {𝐴})
6159, 60anbi12i 629 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
6255, 61bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
63 brun 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65 opelxp 5668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ Limits ))
6612, 65mpbiran 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 ∈ Limits )
6739ellimits 36124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ Limits ↔ Lim 𝑦)
6866, 67bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69 opex 5419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⟨𝑓, 𝑦⟩ ∈ V
7069, 26brco 5827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥))
71 vex 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑧 ∈ V
7212, 39, 71brimg 36151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩Img𝑧 ↔ 𝑧 = (𝑓 “ 𝑦))
7326brbigcup 36112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 Bigcup 𝑥 ↔ ∪ 𝑧 = 𝑥)
7472, 73anbi12i 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
7574exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
7612imaex 7866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 “ 𝑦) ∈ V
77 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓 “ 𝑦) → ∪ 𝑧 = ∪ (𝑓 “ 𝑦))
7877eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓 “ 𝑦) → (∪ 𝑧 = 𝑥 ↔ ∪ (𝑓 “ 𝑦) = 𝑥))
7976, 78ceqsexv 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ ∪ (𝑓 “ 𝑦) = 𝑥)
80 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∪ (𝑓 “ 𝑦) = 𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
8179, 80bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
8270, 75, 813bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
8368, 82anbi12i 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
8464, 83bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
8526brresi 5955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86 opelxp 5668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
8712, 86mpbiran 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
8839elrn 5850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
8971, 39brsuccf 36156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧Succ𝑦 ↔ 𝑦 = suc 𝑧)
9089exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
9187, 88, 903bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
9269, 26brco 5827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥))
93 vex 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑎 ∈ V
9469, 93brco 5827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎))
9512, 39, 71brpprod3a 36100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏))
96 3anrot 1100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
9793ideq 5809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 I 𝑎 ↔ 𝑓 = 𝑎)
98 equcom 2020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓 = 𝑎 ↔ 𝑎 = 𝑓)
9997, 98bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑓 I 𝑎 ↔ 𝑎 = 𝑓)
100 vex 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 𝑏 ∈ V
101100brbigcup 36112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 Bigcup 𝑏 ↔ ∪ 𝑦 = 𝑏)
102 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (∪ 𝑦 = 𝑏 ↔ 𝑏 = ∪ 𝑦)
103101, 102bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 Bigcup 𝑏 ↔ 𝑏 = ∪ 𝑦)
104 biid 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
10599, 103, 1043anbi123i 1156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
10696, 105bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
1071062exbii 1851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
108 vuniex 7694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ∪ 𝑦 ∈ V
109 opeq1 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110109eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111 opeq2 4832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑏 = ∪ 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, ∪ 𝑦⟩)
112111eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = ∪ 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩))
11312, 108, 110, 112ceqsex2v 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
11495, 107, 1133bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
115114anbi1i 625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
116115exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
117 opex 5419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⟨𝑓, ∪ 𝑦⟩ ∈ V
118 breq1 5103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = ⟨𝑓, ∪ 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎))
119117, 118ceqsexv 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎)
12012, 108, 93brapply 36152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟨𝑓, ∪ 𝑦⟩Apply𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
121119, 120bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓‘∪ 𝑦))
12294, 116, 1213bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
12393, 26brfullfun 36164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎FullFun𝐹𝑥 ↔ 𝑥 = (𝐹‘𝑎))
124122, 123anbi12i 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
125124exbii 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
126 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓‘∪ 𝑦) ∈ V
127 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 = (𝑓‘∪ 𝑦) → (𝐹‘𝑎) = (𝐹‘(𝑓‘∪ 𝑦)))
128127eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 = (𝑓‘∪ 𝑦) → (𝑥 = (𝐹‘𝑎) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
129126, 128ceqsexv 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
13092, 125, 1293bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
13191, 130anbi12i 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 915 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 915 . . . . . . . . . . . . . . . . . . . . . . . . 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 7798 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138 nlim0 6385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim ∅
139 limeq 6337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140138, 139mtbiri 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ Lim 𝑦)
141140intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
142 nsuceq0 6410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 suc 𝑧 ≠ ∅
143 neeq2 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = ∅ → (suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅))
144142, 143mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = ∅ → suc 𝑧 ≠ 𝑦)
145144necomd 2988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146145neneqd 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147146nexdv 1938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148147intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
149 ioran 986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
150141, 148, 149sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = ∅ → ¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
151 orel2 891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
153 iftrue 4487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154 unisnif 36139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155153, 154eqtr4di 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ {𝐴})
156155eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 868 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166142, 165mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → 𝑦 ≠ ∅)
167166neneqd 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168167intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
169168rexlimivw 3135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
170 orel1 889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
172 nlimsucg 7794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ V → ¬ Lim suc 𝑧)
173172elv 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ Lim suc 𝑧
174 limeq 6337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175173, 174mtbiri 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176175rexlimivw 3135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177176intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
178 orel1 889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
180142neii 2935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ¬ suc 𝑧 = ∅
181180iffalsei 4491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
182 iffalse 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
18371, 172, 182mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
184181, 183eqtri 2760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
185 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
187186fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
188187fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
189174, 188ifbieq2d 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
190185, 189ifbieq2d 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
191184, 190, 1883eqtr4a 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
192191rexlimivw 3135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
193192eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198193biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
199 olc 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
200199olcd 875 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
201197, 198, 200syl6an 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207206con2i 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208207intnanrd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
209 orel2 891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Lim 𝑦 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
211203iffalsed 4492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
212 iftrue 4487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
213211, 212eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ (𝑓 “ 𝑦))
214213eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
222221olcd 875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1431 . . . . . . . . . . . . . . . . . . . . . . . . 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 5839 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
23112, 39, 26brapply 36152 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
232230, 231bitri 275 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦))
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦)))
234229, 233anbi12d 633 . . . . . . . . . . . . . . . . . . . . 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 1923 . . . . . . . . . . . . . . . . . . 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 5101 . . . . . . . . . . . . . . . . . . . 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 36117 . . . . . . . . . . . . . . . . . . . 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 5827 . . . . . . . . . . . . . . . . . . . 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 6855 . . . . . . . . . . . . . . . . . . . 20 (𝑓‘𝑦) ∈ V
242241eqvinc 3605 . . . . . . . . . . . . . . . . . . 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 1122 . . . . . . . . . . . . . . . 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 1923 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ ∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
251 exnal 1829 . . . . . . . . . . . 12 (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
252250, 251bitr2di 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 5857 . . . . . . . . . . 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 3053 . . . . . . . . 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 2872 . . 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 4877 . 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 2763 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 848   ∨ w3o 1086   ∧ w3a 1087  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902  ∅c0 4287  ifcif 4481  {csn 4582  ⟨cop 4588  ∪ cuni 4865   class class class wbr 5100   I cid 5526   E cep 5531   × cxp 5630  ◡ccnv 5631  dom cdm 5632  ran crn 5633   ↾ cres 5634   “ cima 5635   ∘ ccom 5636  Oncon0 6325  Lim wlim 6326  suc csuc 6327  Fun wfun 6494   Fn wfn 6495  ‘cfv 6500  reccrdg 8350  pprodcpprod 36045   Bigcup cbigcup 36048   Fix cfix 36049   Limits climits 36050   Funs cfuns 36051  Imgcimg 36056  Domaincdomain 36057  Applycapply 36059  Succcsuccf 36062  FullFuncfullfn 36064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-symdif 4207  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-txp 36068  df-pprod 36069  df-bigcup 36072  df-fix 36073  df-limits 36074  df-funs 36075  df-singleton 36076  df-singles 36077  df-image 36078  df-cart 36079  df-img 36080  df-domain 36081  df-cup 36083  df-succf 36086  df-apply 36087  df-funpart 36088  df-fullfun 36089
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator