Step | Hyp | Ref
| Expression |
1 | | dfrdg3 30946 |
. 2
⊢ rec(𝐹, 𝐴) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
2 | | an12 834 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
3 | | df-fn 5807 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥)) |
4 | | ancom 465 |
. . . . . . . . . 10
⊢ ((Fun
𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓)) |
5 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓) |
6 | 5 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((dom
𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓)) |
7 | 3, 4, 6 | 3bitri 285 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓)) |
8 | 7 | anbi1i 727 |
. . . . . . . 8
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
9 | | anass 679 |
. . . . . . . 8
⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
10 | 2, 8, 9 | 3bitri 285 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
11 | 10 | exbii 1764 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
12 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
13 | 12 | dmex 6991 |
. . . . . . 7
⊢ dom 𝑓 ∈ V |
14 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On)) |
15 | | raleq 3115 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
16 | 14, 15 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
17 | 16 | anbi2d 736 |
. . . . . . 7
⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
18 | 13, 17 | ceqsexv 3215 |
. . . . . 6
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
19 | 11, 18 | bitri 263 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
20 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
21 | | eldif 3550 |
. . . . . 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 3758 |
. . . . . . . 8
⊢ (𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On))) |
23 | 12 | elfuns 31192 |
. . . . . . . . 9
⊢ (𝑓 ∈
Funs ↔ Fun 𝑓) |
24 | 12 | elima 5390 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓) |
25 | | df-rex 2902 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ On
𝑥◡Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓)) |
26 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥◡Domain𝑓 ∧ 𝑥 ∈ On)) |
27 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
28 | 27, 12 | brcnv 5227 |
. . . . . . . . . . . . . . 15
⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥) |
29 | 12, 27 | brdomain 31210 |
. . . . . . . . . . . . . . 15
⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓) |
30 | 28, 29 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓) |
31 | 30 | anbi1i 727 |
. . . . . . . . . . . . 13
⊢ ((𝑥◡Domain𝑓 ∧ 𝑥 ∈ On) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On)) |
32 | 26, 31 | bitri 263 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On)) |
33 | 32 | exbii 1764 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On)) |
34 | 13, 14 | ceqsexv 3215 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On) ↔ dom 𝑓 ∈ On) |
35 | 33, 34 | bitri 263 |
. . . . . . . . . 10
⊢
(∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ dom 𝑓 ∈ On) |
36 | 24, 25, 35 | 3bitri 285 |
. . . . . . . . 9
⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On) |
37 | 23, 36 | anbi12i 729 |
. . . . . . . 8
⊢ ((𝑓 ∈
Funs ∧ 𝑓 ∈
(◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) |
38 | 22, 37 | bitri 263 |
. . . . . . 7
⊢ (𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ↔ (Fun 𝑓 ∧
dom 𝑓 ∈
On)) |
39 | 38 | anbi1i 727 |
. . . . . 6
⊢ ((𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ∧ ¬ 𝑓 ∈
dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔
((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran
Succ)))))))) |
40 | | brdif 4635 |
. . . . . . . . . . . . . . 15
⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ (𝑓(◡ E
∘ Domain)𝑦 ∧
¬ 𝑓 Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦)) |
41 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
42 | 12, 41 | brco 5214 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦)) |
43 | 29 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦)) |
44 | 43 | exbii 1764 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦)) |
45 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = dom 𝑓 → (𝑥◡ E
𝑦 ↔ dom 𝑓◡ E 𝑦)) |
46 | 13, 45 | ceqsexv 3215 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦) ↔ dom 𝑓◡ E 𝑦) |
47 | 44, 46 | bitri 263 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ dom 𝑓◡ E 𝑦) |
48 | 13, 41 | brcnv 5227 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓) |
49 | 13 | epelc 4951 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓) |
50 | 48, 49 | bitri 263 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓) |
51 | 42, 47, 50 | 3bitri 285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓) |
52 | 51 | anbi1i 727 |
. . . . . . . . . . . . . . 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)))))𝑦)) |
53 | 40, 52 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))))𝑦)) |
54 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((dom
𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On) |
55 | 54 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On) |
56 | | brun 4633 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈𝑓, 𝑦〉(((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥
↔ (〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ∨ 〈𝑓, 𝑦〉((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))𝑥)) |
57 | | brxp 5071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ↔ (〈𝑓, 𝑦〉 ∈ (V × {∅}) ∧
𝑥 ∈ {∪ {𝐴}})) |
58 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ↔ (𝑓 ∈
V ∧ 𝑦 ∈
{∅})) |
59 | 12, 58 | mpbiran 955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ↔ 𝑦 ∈
{∅}) |
60 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
61 | 59, 60 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ↔ 𝑦 =
∅) |
62 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ {∪ {𝐴}}
↔ 𝑥 = ∪ {𝐴}) |
63 | 61, 62 | anbi12i 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ∧ 𝑥 ∈
{∪ {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
64 | 57, 63 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
65 | | brun 4633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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))𝑥)) |
66 | 27 | brres 5323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑓, 𝑦〉((
Bigcup ∘ Img) ↾ (V × Limits
))𝑥 ↔
(〈𝑓, 𝑦〉(
Bigcup ∘ Img)𝑥 ∧ 〈𝑓, 𝑦〉 ∈ (V × Limits ))) |
67 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
〈𝑓, 𝑦〉 ∈ V |
68 | 67, 27 | brco 5214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉(
Bigcup ∘ Img)𝑥 ↔ ∃𝑧(〈𝑓, 𝑦〉Img𝑧 ∧ 𝑧 Bigcup 𝑥)) |
69 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝑧 ∈ V |
70 | 12, 41, 69 | brimg 31214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(〈𝑓, 𝑦〉Img𝑧 ↔ 𝑧 = (𝑓 “ 𝑦)) |
71 | 27 | brbigcup 31175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 Bigcup
𝑥 ↔ ∪ 𝑧 =
𝑥) |
72 | 70, 71 | anbi12i 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((〈𝑓, 𝑦〉Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥)) |
73 | 72 | exbii 1764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧(〈𝑓, 𝑦〉Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥)) |
74 | | imaexg 6995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 ∈ V → (𝑓 “ 𝑦) ∈ V) |
75 | 12, 74 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 “ 𝑦) ∈ V |
76 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 = (𝑓 “ 𝑦) → ∪ 𝑧 = ∪
(𝑓 “ 𝑦)) |
77 | 76 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = (𝑓 “ 𝑦) → (∪ 𝑧 = 𝑥 ↔ ∪ (𝑓 “ 𝑦) = 𝑥)) |
78 | 75, 77 | ceqsexv 3215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ ∪ (𝑓 “ 𝑦) = 𝑥) |
79 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (∪ (𝑓
“ 𝑦) = 𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦)) |
80 | 78, 79 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ 𝑥 = ∪ (𝑓 “ 𝑦)) |
81 | 68, 73, 80 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉(
Bigcup ∘ Img)𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦)) |
82 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ Limits
)) |
83 | 12, 82 | mpbiran 955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ↔ 𝑦 ∈ Limits
) |
84 | 41 | ellimits 31187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈
Limits ↔ Lim 𝑦) |
85 | 83, 84 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ↔ Lim 𝑦) |
86 | 81, 85 | anbi12ci 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((〈𝑓, 𝑦〉(
Bigcup ∘ Img)𝑥 ∧ 〈𝑓, 𝑦〉 ∈ (V × Limits )) ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
87 | 66, 86 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑓, 𝑦〉((
Bigcup ∘ Img) ↾ (V × Limits
))𝑥 ↔ (Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
88 | 27 | brres 5323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑓, 𝑦〉((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ∧ 〈𝑓, 𝑦〉 ∈ (V × ran
Succ))) |
89 | 67, 27 | brco 5214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(〈𝑓, 𝑦〉(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥)) |
90 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 𝑎 ∈ V |
91 | 67, 90 | brco 5214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(〈𝑓, 𝑦〉(Apply ∘ pprod( I ,
Bigcup ))𝑎 ↔ ∃𝑧(〈𝑓, 𝑦〉pprod( I ,
Bigcup )𝑧 ∧
𝑧Apply𝑎)) |
92 | 12, 41, 69 | brpprod3a 31163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(〈𝑓, 𝑦〉pprod( I , Bigcup )𝑧 ↔ ∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏)) |
93 | | 3anrot 1036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
94 | 90 | ideq 5196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓 I 𝑎 ↔ 𝑓 = 𝑎) |
95 | | equcom 1932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓 = 𝑎 ↔ 𝑎 = 𝑓) |
96 | 94, 95 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑓 I 𝑎 ↔ 𝑎 = 𝑓) |
97 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ 𝑏 ∈ V |
98 | 97 | brbigcup 31175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 Bigcup
𝑏 ↔ ∪ 𝑦 =
𝑏) |
99 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (∪ 𝑦 =
𝑏 ↔ 𝑏 = ∪ 𝑦) |
100 | 98, 99 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 Bigcup
𝑏 ↔ 𝑏 = ∪
𝑦) |
101 | | biid 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝑎, 𝑏〉) |
102 | 96, 100, 101 | 3anbi123i 1244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
103 | 93, 102 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
104 | 103 | 2exbii 1765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
105 | | vuniex 6852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ∪ 𝑦
∈ V |
106 | | opeq1 4340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 = 𝑓 → 〈𝑎, 𝑏〉 = 〈𝑓, 𝑏〉) |
107 | 106 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑎 = 𝑓 → (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝑓, 𝑏〉)) |
108 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑏 = ∪
𝑦 → 〈𝑓, 𝑏〉 = 〈𝑓, ∪ 𝑦〉) |
109 | 108 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑏 = ∪
𝑦 → (𝑧 = 〈𝑓, 𝑏〉 ↔ 𝑧 = 〈𝑓, ∪ 𝑦〉)) |
110 | 12, 105, 107, 109 | ceqsex2v 3218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ 𝑧 = 〈𝑓, ∪ 𝑦〉) |
111 | 92, 104, 110 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(〈𝑓, 𝑦〉pprod( I , Bigcup )𝑧 ↔ 𝑧 = 〈𝑓, ∪ 𝑦〉) |
112 | 111 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((〈𝑓, 𝑦〉pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ (𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎)) |
113 | 112 | exbii 1764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑧(〈𝑓, 𝑦〉pprod( I ,
Bigcup )𝑧 ∧
𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎)) |
114 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
〈𝑓, ∪ 𝑦〉 ∈ V |
115 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 = 〈𝑓, ∪ 𝑦〉 → (𝑧Apply𝑎 ↔ 〈𝑓, ∪ 𝑦〉Apply𝑎)) |
116 | 114, 115 | ceqsexv 3215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(∃𝑧(𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎) ↔ 〈𝑓, ∪ 𝑦〉Apply𝑎) |
117 | 12, 105, 90 | brapply 31215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(〈𝑓, ∪ 𝑦〉Apply𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦)) |
118 | 116, 117 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑧(𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓‘∪ 𝑦)) |
119 | 91, 113, 118 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(〈𝑓, 𝑦〉(Apply ∘ pprod( I ,
Bigcup ))𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦)) |
120 | 90, 27 | brfullfun 31225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎FullFun𝐹𝑥 ↔ 𝑥 = (𝐹‘𝑎)) |
121 | 119, 120 | anbi12i 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((〈𝑓, 𝑦〉(Apply ∘ pprod( I ,
Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎))) |
122 | 121 | exbii 1764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑎(〈𝑓, 𝑦〉(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎))) |
123 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓‘∪ 𝑦)
∈ V |
124 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝐹‘𝑎) = (𝐹‘(𝑓‘∪ 𝑦))) |
125 | 124 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝑥 = (𝐹‘𝑎) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
126 | 123, 125 | ceqsexv 3215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) |
127 | 89, 122, 126 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) |
128 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ↔ (𝑓 ∈ V
∧ 𝑦 ∈ ran
Succ)) |
129 | 12, 128 | mpbiran 955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ↔ 𝑦 ∈ ran
Succ) |
130 | 41 | elrn 5287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ran Succ ↔
∃𝑧 𝑧Succ𝑦) |
131 | 69, 41 | brsuccf 31218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧Succ𝑦 ↔ 𝑦 = suc 𝑧) |
132 | 131 | exbii 1764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧) |
133 | 129, 130,
132 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ↔ ∃𝑧 𝑦 = suc 𝑧) |
134 | 127, 133 | anbi12ci 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ∧ 〈𝑓, 𝑦〉 ∈ (V × ran Succ)) ↔
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
135 | 88, 134 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑓, 𝑦〉((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
136 | 87, 135 | orbi12i 542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑓, 𝑦〉((
Bigcup ∘ Img) ↾ (V × Limits
))𝑥 ∨ 〈𝑓, 𝑦〉((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
137 | 65, 136 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑓, 𝑦〉(((
Bigcup ∘ Img) ↾ (V × Limits
)) ∪ ((FullFun𝐹
∘ (Apply ∘ pprod( I , Bigcup )))
↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
138 | 64, 137 | orbi12i 542 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ∨ 〈𝑓, 𝑦〉((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))𝑥)
↔ ((𝑦 = ∅ ∧
𝑥 = ∪ {𝐴})
∨ ((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
139 | 56, 138 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑓, 𝑦〉(((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥
↔ ((𝑦 = ∅ ∧
𝑥 = ∪ {𝐴})
∨ ((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
140 | | onzsl 6938 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦))) |
141 | | nlim0 5700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ¬
Lim ∅ |
142 | | limeq 5652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → (Lim 𝑦 ↔ Lim
∅)) |
143 | 141, 142 | mtbiri 316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → ¬ Lim
𝑦) |
144 | 143 | intnanrd 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → ¬ (Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
145 | | nsuceq0 5722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ suc 𝑧 ≠ ∅ |
146 | | neeq2 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = ∅ → (suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅)) |
147 | 145, 146 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = ∅ → suc 𝑧 ≠ 𝑦) |
148 | 147 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = ∅ → 𝑦 ≠ suc 𝑧) |
149 | 148 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧) |
150 | 149 | nexdv 1851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → ¬
∃𝑧 𝑦 = suc 𝑧) |
151 | 150 | intnanrd 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → ¬
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
152 | | ioran 510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (¬
((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
153 | 144, 151,
152 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = ∅ → ¬ ((Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
154 | | orel2 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))) |
156 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅)) |
157 | | unisnif 31202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ∪ {𝐴}
= if(𝐴 ∈ V, 𝐴, ∅) |
158 | 156, 157 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ {𝐴}) |
159 | 158 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ {𝐴})) |
160 | 159 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = ∅ → (𝑥 = ∪
{𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
161 | 160 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
162 | 155, 161 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
163 | 159 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ {𝐴})) |
164 | 163 | anc2li 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))) |
165 | | orc 399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
166 | 164, 165 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
167 | 162, 166 | impbid 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
168 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅)) |
169 | 145, 168 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = suc 𝑧 → 𝑦 ≠ ∅) |
170 | 169 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅) |
171 | 170 | intnanrd 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
172 | 171 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
173 | | orel1 396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
(𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
175 | | nlimsucg 6934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ V → ¬ Lim suc
𝑧) |
176 | 69, 175 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ¬
Lim suc 𝑧 |
177 | | limeq 5652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧)) |
178 | 176, 177 | mtbiri 316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = suc 𝑧 → ¬ Lim 𝑦) |
179 | 178 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ¬ Lim 𝑦) |
180 | 179 | intnanrd 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
181 | | orel1 396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
(Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
183 | 145 | neii 2784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ¬
suc 𝑧 =
∅ |
184 | 183 | iffalsei 4046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ if(suc
𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) |
185 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (¬
Lim suc 𝑧 → if(Lim suc
𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
186 | 69, 175, 185 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ if(Lim
suc 𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)) |
187 | 184, 186 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ if(suc
𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧)) |
188 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅)) |
189 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪
suc 𝑧) |
190 | 189 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧)) |
191 | 190 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
192 | 177, 191 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) |
193 | 188, 192 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))) |
194 | 187, 193,
191 | 3eqtr4a 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦))) |
195 | 194 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦))) |
196 | 195 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
197 | 196 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓‘∪ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
198 | 197 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
199 | 174, 182,
198 | 3syld 58 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
200 | | rexex 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧) |
201 | 196 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
202 | | olc 398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
203 | 202 | olcd 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
204 | 200, 201,
203 | syl6an 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
205 | 199, 204 | impbid 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
206 | 143 | con2i 133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 → ¬ 𝑦 = ∅) |
207 | 206 | intnanrd 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴})) |
208 | 207, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
209 | 178 | exlimiv 1845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦) |
210 | 209 | con2i 133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧) |
211 | 210 | intnanrd 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → ¬
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
212 | | orel2 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (¬
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))) |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))) |
214 | 206 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (Lim
𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) |
215 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (Lim
𝑦 → if(Lim 𝑦, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓
“ 𝑦)) |
216 | 214, 215 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (Lim
𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ (𝑓
“ 𝑦)) |
217 | 216 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ (𝑓 “ 𝑦))) |
218 | 217 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → (𝑥 = ∪
(𝑓 “ 𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
219 | 218 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
220 | 208, 213,
219 | 3syld 58 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Lim
𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
221 | 220 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
222 | 217 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ (𝑓 “ 𝑦))) |
223 | 222 | anc2li 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))) |
224 | | orc 399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
225 | 224 | olcd 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
226 | 223, 225 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
227 | 226 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
228 | 221, 227 | impbid 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
229 | 167, 205,
228 | 3jaoi 1383 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
230 | 140, 229 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
231 | 139, 230 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ On → (〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥
↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
232 | 55, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥
↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
233 | 27, 67 | brcnv 5227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 〈𝑓, 𝑦〉Apply𝑥) |
234 | 12, 41, 27 | brapply 31215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑓, 𝑦〉Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦)) |
235 | 233, 234 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 𝑥 = (𝑓‘𝑦)) |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 𝑥 = (𝑓‘𝑦))) |
237 | 232, 236 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥 ∧
𝑥◡Apply〈𝑓, 𝑦〉) ↔ (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ∧ 𝑥 = (𝑓‘𝑦)))) |
238 | | ancom 465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ∧ 𝑥 = (𝑓‘𝑦)) ↔ (𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
239 | 237, 238 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥 ∧
𝑥◡Apply〈𝑓, 𝑦〉) ↔ (𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
240 | 239 | exbidv 1837 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (∃𝑥(〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥 ∧
𝑥◡Apply〈𝑓, 𝑦〉) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
241 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . . 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)))))) |
242 | 67 | elfix 31180 |
. . . . . . . . . . . . . . . . . . . 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)))))〈𝑓, 𝑦〉) |
243 | 67, 67 | brco 5214 |
. . . . . . . . . . . . . . . . . . . 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〈𝑓, 𝑦〉)) |
244 | 241, 242,
243 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 Fix
(◡Apply ∘ (((V ×
{∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))))𝑦
↔ ∃𝑥(〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥 ∧
𝑥◡Apply〈𝑓, 𝑦〉)) |
245 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓‘𝑦) ∈ V |
246 | 245 | eqvinc 3300 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
247 | 240, 244,
246 | 3bitr4g 302 |
. . . . . . . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
248 | 247 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (¬ 𝑓 Fix (◡Apply ∘ (((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))))𝑦
↔ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
249 | 248 | 3expia 1259 |
. . . . . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
250 | 249 | pm5.32d 669 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On) → ((𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))))𝑦)
↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
251 | | annim 440 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
252 | 250, 251 | syl6bb 275 |
. . . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
253 | 53, 252 | syl5bb 271 |
. . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
254 | 253 | exbidv 1837 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On) → (∃𝑦 𝑓((◡ E
∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))))𝑦
↔ ∃𝑦 ¬
(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
255 | | exnal 1744 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ¬
(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
256 | 254, 255 | syl6rbb 276 |
. . . . . . . . . . 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))))))𝑦)) |
257 | 12 | eldm 5243 |
. . . . . . . . . . 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))))))𝑦) |
258 | 256, 257 | syl6bbr 277 |
. . . . . . . . . 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)))))))) |
259 | 258 | con1bid 344 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On) → (¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔
∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
260 | | df-ral 2901 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
261 | 259, 260 | syl6bbr 277 |
. . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
262 | 261 | pm5.32i 667 |
. . . . . . 7
⊢ (((Fun
𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔
((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
263 | | anass 679 |
. . . . . . 7
⊢ (((Fun
𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
264 | 262, 263 | bitri 263 |
. . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
265 | 21, 39, 264 | 3bitri 285 |
. . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
266 | 19, 20, 265 | 3bitr4ri 292 |
. . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
267 | 266 | abbi2i 2725 |
. . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
268 | 267 | unieqi 4381 |
. 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
269 | 1, 268 | eqtr4i 2635 |
1
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran
Succ))))))) |