Step | Hyp | Ref
| Expression |
1 | | dfrdg3 33344 |
. 2
⊢ rec(𝐹, 𝐴) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
2 | | an12 645 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
3 | | df-fn 6342 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥)) |
4 | | ancom 464 |
. . . . . . . . . 10
⊢ ((Fun
𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓)) |
5 | | eqcom 2745 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓) |
6 | 5 | anbi1i 627 |
. . . . . . . . . 10
⊢ ((dom
𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓)) |
7 | 3, 4, 6 | 3bitri 300 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓)) |
8 | 7 | anbi1i 627 |
. . . . . . . 8
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
9 | | anass 472 |
. . . . . . . 8
⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
10 | 2, 8, 9 | 3bitri 300 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
11 | 10 | exbii 1854 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
12 | | vex 3402 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
13 | 12 | dmex 7642 |
. . . . . . 7
⊢ dom 𝑓 ∈ V |
14 | | eleq1 2820 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On)) |
15 | | raleq 3310 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
16 | 14, 15 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
17 | 16 | anbi2d 632 |
. . . . . . 7
⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))) |
18 | 13, 17 | ceqsexv 3445 |
. . . . . 6
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
19 | 11, 18 | bitri 278 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
20 | | df-rex 3059 |
. . . . 5
⊢
(∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
21 | | eldif 3853 |
. . . . . 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 3859 |
. . . . . . . 8
⊢ (𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On))) |
23 | 12 | elfuns 33855 |
. . . . . . . . 9
⊢ (𝑓 ∈
Funs ↔ Fun 𝑓) |
24 | 12 | elima 5908 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓) |
25 | | df-rex 3059 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ On
𝑥◡Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓)) |
26 | | vex 3402 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
27 | 26, 12 | brcnv 5725 |
. . . . . . . . . . . . . 14
⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥) |
28 | 12, 26 | brdomain 33873 |
. . . . . . . . . . . . . 14
⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓) |
29 | 27, 28 | bitri 278 |
. . . . . . . . . . . . 13
⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓) |
30 | 29 | anbi1ci 629 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On)) |
31 | 30 | exbii 1854 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On)) |
32 | 13, 14 | ceqsexv 3445 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On) ↔ dom 𝑓 ∈ On) |
33 | 31, 32 | bitri 278 |
. . . . . . . . . 10
⊢
(∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ dom 𝑓 ∈ On) |
34 | 24, 25, 33 | 3bitri 300 |
. . . . . . . . 9
⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On) |
35 | 23, 34 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑓 ∈
Funs ∧ 𝑓 ∈
(◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) |
36 | 22, 35 | bitri 278 |
. . . . . . 7
⊢ (𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ↔ (Fun 𝑓 ∧
dom 𝑓 ∈
On)) |
37 | 36 | anbi1i 627 |
. . . . . 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 5083 |
. . . . . . . . . . . . . . 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 3402 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
40 | 12, 39 | brco 5713 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦)) |
41 | 28 | anbi1i 627 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦)) |
42 | 41 | exbii 1854 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦)) |
43 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = dom 𝑓 → (𝑥◡ E
𝑦 ↔ dom 𝑓◡ E 𝑦)) |
44 | 13, 43 | ceqsexv 3445 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦) ↔ dom 𝑓◡ E 𝑦) |
45 | 42, 44 | bitri 278 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ dom 𝑓◡ E 𝑦) |
46 | 13, 39 | brcnv 5725 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓) |
47 | 13 | epeli 5436 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓) |
48 | 46, 47 | bitri 278 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓) |
49 | 40, 45, 48 | 3bitri 300 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓) |
50 | 49 | anbi1i 627 |
. . . . . . . . . . . . . . 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)))))𝑦)) |
51 | 38, 50 | bitri 278 |
. . . . . . . . . . . . . 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 6197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((dom
𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On) |
53 | 52 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On) |
54 | | brun 5081 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 5572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ↔ (〈𝑓, 𝑦〉 ∈ (V × {∅}) ∧
𝑥 ∈ {∪ {𝐴}})) |
56 | | opelxp 5561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ↔ (𝑓 ∈
V ∧ 𝑦 ∈
{∅})) |
57 | 12, 56 | mpbiran 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ↔ 𝑦 ∈
{∅}) |
58 | | velsn 4532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
59 | 57, 58 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ↔ 𝑦 =
∅) |
60 | | velsn 4532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ {∪ {𝐴}}
↔ 𝑥 = ∪ {𝐴}) |
61 | 59, 60 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑓, 𝑦〉 ∈ (V ×
{∅}) ∧ 𝑥 ∈
{∪ {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
62 | 55, 61 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
63 | | brun 5081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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))𝑥)) |
64 | 26 | brresi 5834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑓, 𝑦〉((
Bigcup ∘ Img) ↾ (V × Limits
))𝑥 ↔
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ∧ 〈𝑓, 𝑦〉( Bigcup
∘ Img)𝑥)) |
65 | | opelxp 5561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ Limits
)) |
66 | 12, 65 | mpbiran 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ↔ 𝑦 ∈ Limits
) |
67 | 39 | ellimits 33850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈
Limits ↔ Lim 𝑦) |
68 | 66, 67 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉 ∈ (V × Limits ) ↔ Lim 𝑦) |
69 | | opex 5322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
〈𝑓, 𝑦〉 ∈ V |
70 | 69, 26 | brco 5713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉(
Bigcup ∘ Img)𝑥 ↔ ∃𝑧(〈𝑓, 𝑦〉Img𝑧 ∧ 𝑧 Bigcup 𝑥)) |
71 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝑧 ∈ V |
72 | 12, 39, 71 | brimg 33877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(〈𝑓, 𝑦〉Img𝑧 ↔ 𝑧 = (𝑓 “ 𝑦)) |
73 | 26 | brbigcup 33838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 Bigcup
𝑥 ↔ ∪ 𝑧 =
𝑥) |
74 | 72, 73 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((〈𝑓, 𝑦〉Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥)) |
75 | 74 | exbii 1854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧(〈𝑓, 𝑦〉Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥)) |
76 | 12 | imaex 7647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 “ 𝑦) ∈ V |
77 | | unieq 4807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 = (𝑓 “ 𝑦) → ∪ 𝑧 = ∪
(𝑓 “ 𝑦)) |
78 | 77 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = (𝑓 “ 𝑦) → (∪ 𝑧 = 𝑥 ↔ ∪ (𝑓 “ 𝑦) = 𝑥)) |
79 | 76, 78 | ceqsexv 3445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ ∪ (𝑓 “ 𝑦) = 𝑥) |
80 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (∪ (𝑓
“ 𝑦) = 𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦)) |
81 | 79, 80 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ 𝑥 = ∪ (𝑓 “ 𝑦)) |
82 | 70, 75, 81 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉(
Bigcup ∘ Img)𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦)) |
83 | 68, 82 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((〈𝑓, 𝑦〉 ∈ (V × Limits ) ∧ 〈𝑓, 𝑦〉( Bigcup
∘ Img)𝑥) ↔ (Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
84 | 64, 83 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑓, 𝑦〉((
Bigcup ∘ Img) ↾ (V × Limits
))𝑥 ↔ (Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
85 | 26 | brresi 5834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑓, 𝑦〉((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (〈𝑓, 𝑦〉 ∈ (V × ran Succ) ∧
〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥)) |
86 | | opelxp 5561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ↔ (𝑓 ∈ V
∧ 𝑦 ∈ ran
Succ)) |
87 | 12, 86 | mpbiran 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ↔ 𝑦 ∈ ran
Succ) |
88 | 39 | elrn 5736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ran Succ ↔
∃𝑧 𝑧Succ𝑦) |
89 | 71, 39 | brsuccf 33881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧Succ𝑦 ↔ 𝑦 = suc 𝑧) |
90 | 89 | exbii 1854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧) |
91 | 87, 88, 90 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ↔ ∃𝑧 𝑦 = suc 𝑧) |
92 | 69, 26 | brco 5713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(〈𝑓, 𝑦〉(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥)) |
93 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 𝑎 ∈ V |
94 | 69, 93 | brco 5713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(〈𝑓, 𝑦〉(Apply ∘ pprod( I ,
Bigcup ))𝑎 ↔ ∃𝑧(〈𝑓, 𝑦〉pprod( I ,
Bigcup )𝑧 ∧
𝑧Apply𝑎)) |
95 | 12, 39, 71 | brpprod3a 33826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(〈𝑓, 𝑦〉pprod( I , Bigcup )𝑧 ↔ ∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏)) |
96 | | 3anrot 1101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
97 | 93 | ideq 5695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓 I 𝑎 ↔ 𝑓 = 𝑎) |
98 | | equcom 2030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓 = 𝑎 ↔ 𝑎 = 𝑓) |
99 | 97, 98 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑓 I 𝑎 ↔ 𝑎 = 𝑓) |
100 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ 𝑏 ∈ V |
101 | 100 | brbigcup 33838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 Bigcup
𝑏 ↔ ∪ 𝑦 =
𝑏) |
102 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (∪ 𝑦 =
𝑏 ↔ 𝑏 = ∪ 𝑦) |
103 | 101, 102 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 Bigcup
𝑏 ↔ 𝑏 = ∪
𝑦) |
104 | | biid 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝑎, 𝑏〉) |
105 | 99, 103, 104 | 3anbi123i 1156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
106 | 96, 105 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
107 | 106 | 2exbii 1855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
108 | | vuniex 7483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ∪ 𝑦
∈ V |
109 | | opeq1 4759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 = 𝑓 → 〈𝑎, 𝑏〉 = 〈𝑓, 𝑏〉) |
110 | 109 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑎 = 𝑓 → (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝑓, 𝑏〉)) |
111 | | opeq2 4761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑏 = ∪
𝑦 → 〈𝑓, 𝑏〉 = 〈𝑓, ∪ 𝑦〉) |
112 | 111 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑏 = ∪
𝑦 → (𝑧 = 〈𝑓, 𝑏〉 ↔ 𝑧 = 〈𝑓, ∪ 𝑦〉)) |
113 | 12, 108, 110, 112 | ceqsex2v 3448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ 𝑧 = 〈𝑓, ∪ 𝑦〉) |
114 | 95, 107, 113 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(〈𝑓, 𝑦〉pprod( I , Bigcup )𝑧 ↔ 𝑧 = 〈𝑓, ∪ 𝑦〉) |
115 | 114 | anbi1i 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((〈𝑓, 𝑦〉pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ (𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎)) |
116 | 115 | exbii 1854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑧(〈𝑓, 𝑦〉pprod( I ,
Bigcup )𝑧 ∧
𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎)) |
117 | | opex 5322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
〈𝑓, ∪ 𝑦〉 ∈ V |
118 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 = 〈𝑓, ∪ 𝑦〉 → (𝑧Apply𝑎 ↔ 〈𝑓, ∪ 𝑦〉Apply𝑎)) |
119 | 117, 118 | ceqsexv 3445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(∃𝑧(𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎) ↔ 〈𝑓, ∪ 𝑦〉Apply𝑎) |
120 | 12, 108, 93 | brapply 33878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(〈𝑓, ∪ 𝑦〉Apply𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦)) |
121 | 119, 120 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑧(𝑧 = 〈𝑓, ∪ 𝑦〉 ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓‘∪ 𝑦)) |
122 | 94, 116, 121 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(〈𝑓, 𝑦〉(Apply ∘ pprod( I ,
Bigcup ))𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦)) |
123 | 93, 26 | brfullfun 33888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎FullFun𝐹𝑥 ↔ 𝑥 = (𝐹‘𝑎)) |
124 | 122, 123 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((〈𝑓, 𝑦〉(Apply ∘ pprod( I ,
Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎))) |
125 | 124 | exbii 1854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑎(〈𝑓, 𝑦〉(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎))) |
126 | | fvex 6687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓‘∪ 𝑦)
∈ V |
127 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝐹‘𝑎) = (𝐹‘(𝑓‘∪ 𝑦))) |
128 | 127 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝑥 = (𝐹‘𝑎) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
129 | 126, 128 | ceqsexv 3445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) |
130 | 92, 125, 129 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) |
131 | 91, 130 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((〈𝑓, 𝑦〉 ∈ (V × ran
Succ) ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥) ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
132 | 85, 131 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑓, 𝑦〉((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
133 | 84, 132 | orbi12i 914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑓, 𝑦〉((
Bigcup ∘ Img) ↾ (V × Limits
))𝑥 ∨ 〈𝑓, 𝑦〉((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
134 | 63, 133 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑓, 𝑦〉(((
Bigcup ∘ Img) ↾ (V × Limits
)) ∪ ((FullFun𝐹
∘ (Apply ∘ pprod( I , Bigcup )))
↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
135 | 62, 134 | orbi12i 914 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈𝑓, 𝑦〉((V × {∅})
× {∪ {𝐴}})𝑥 ∨ 〈𝑓, 𝑦〉((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ)))𝑥)
↔ ((𝑦 = ∅ ∧
𝑥 = ∪ {𝐴})
∨ ((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
136 | 54, 135 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑓, 𝑦〉(((V × {∅})
× {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥
↔ ((𝑦 = ∅ ∧
𝑥 = ∪ {𝐴})
∨ ((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
137 | | onzsl 7580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦))) |
138 | | nlim0 6230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ¬
Lim ∅ |
139 | | limeq 6184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → (Lim 𝑦 ↔ Lim
∅)) |
140 | 138, 139 | mtbiri 330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → ¬ Lim
𝑦) |
141 | 140 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → ¬ (Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
142 | | nsuceq0 6252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ suc 𝑧 ≠ ∅ |
143 | | neeq2 2997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = ∅ → (suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅)) |
144 | 142, 143 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = ∅ → suc 𝑧 ≠ 𝑦) |
145 | 144 | necomd 2989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = ∅ → 𝑦 ≠ suc 𝑧) |
146 | 145 | neneqd 2939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧) |
147 | 146 | nexdv 1943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → ¬
∃𝑧 𝑦 = suc 𝑧) |
148 | 147 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → ¬
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
149 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (¬
((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
150 | 141, 148,
149 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = ∅ → ¬ ((Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
151 | | orel2 890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
((Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))) |
153 | | iftrue 4420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅)) |
154 | | unisnif 33865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ∪ {𝐴}
= if(𝐴 ∈ V, 𝐴, ∅) |
155 | 153, 154 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ {𝐴}) |
156 | 155 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ {𝐴})) |
157 | 156 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = ∅ → (𝑥 = ∪
{𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
158 | 157 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
159 | 152, 158 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
160 | 156 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ {𝐴})) |
161 | 160 | anc2li 559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))) |
162 | | orc 866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
163 | 161, 162 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
164 | 159, 163 | impbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
165 | | neeq1 2996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅)) |
166 | 142, 165 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = suc 𝑧 → 𝑦 ≠ ∅) |
167 | 166 | neneqd 2939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅) |
168 | 167 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
169 | 168 | rexlimivw 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})) |
170 | | orel1 888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
(𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
172 | | nlimsucg 7576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ V → ¬ Lim suc
𝑧) |
173 | 172 | elv 3404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ¬
Lim suc 𝑧 |
174 | | limeq 6184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧)) |
175 | 173, 174 | mtbiri 330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = suc 𝑧 → ¬ Lim 𝑦) |
176 | 175 | rexlimivw 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ¬ Lim 𝑦) |
177 | 176 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))) |
178 | | orel1 888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
(Lim 𝑦 ∧ 𝑥 = ∪
(𝑓 “ 𝑦)) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
180 | 142 | neii 2936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ¬
suc 𝑧 =
∅ |
181 | 180 | iffalsei 4424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ if(suc
𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) |
182 | | iffalse 4423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (¬
Lim suc 𝑧 → if(Lim suc
𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
183 | 71, 172, 182 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ if(Lim
suc 𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)) |
184 | 181, 183 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ if(suc
𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧)) |
185 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅)) |
186 | | unieq 4807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪
suc 𝑧) |
187 | 186 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧)) |
188 | 187 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
189 | 174, 188 | ifbieq2d 4440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) |
190 | 185, 189 | ifbieq2d 4440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))) |
191 | 184, 190,
188 | 3eqtr4a 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦))) |
192 | 191 | rexlimivw 3192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦))) |
193 | 192 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
194 | 193 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓‘∪ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
195 | 194 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
196 | 171, 179,
195 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
197 | | rexex 3153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧) |
198 | 193 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
199 | | olc 867 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
200 | 199 | olcd 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
201 | 197, 198,
200 | syl6an 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
202 | 196, 201 | impbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
203 | 140 | con2i 141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 → ¬ 𝑦 = ∅) |
204 | 203 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴})) |
205 | 204, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
206 | 175 | exlimiv 1937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦) |
207 | 206 | con2i 141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧) |
208 | 207 | intnanrd 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → ¬
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) |
209 | | orel2 890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (¬
(∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))) |
210 | 208, 209 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))) |
211 | 203 | iffalsed 4425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (Lim
𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) |
212 | | iftrue 4420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (Lim
𝑦 → if(Lim 𝑦, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓
“ 𝑦)) |
213 | 211, 212 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (Lim
𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ (𝑓
“ 𝑦)) |
214 | 213 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ (𝑓 “ 𝑦))) |
215 | 214 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → (𝑥 = ∪
(𝑓 “ 𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
216 | 215 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
217 | 205, 210,
216 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Lim
𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
218 | 217 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
219 | 214 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ (𝑓 “ 𝑦))) |
220 | 219 | anc2li 559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))) |
221 | | orc 866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) |
222 | 221 | olcd 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Lim
𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))) |
223 | 220, 222 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Lim
𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
224 | 223 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))) |
225 | 218, 224 | impbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
226 | 164, 202,
225 | 3jaoi 1428 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
227 | 137, 226 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = ∪
{𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
228 | 136, 227 | syl5bb 286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ On → (〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥
↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
229 | 53, 228 | 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
230 | 26, 69 | brcnv 5725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 〈𝑓, 𝑦〉Apply𝑥) |
231 | 12, 39, 26 | brapply 33878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑓, 𝑦〉Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦)) |
232 | 230, 231 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 𝑥 = (𝑓‘𝑦)) |
233 | 232 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 𝑥 = (𝑓‘𝑦))) |
234 | 229, 233 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥 ∧
𝑥◡Apply〈𝑓, 𝑦〉) ↔ (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ∧ 𝑥 = (𝑓‘𝑦)))) |
235 | 234 | biancomd 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((〈𝑓, 𝑦〉(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup
∘ Img) ↾ (V × Limits ))
∪ ((FullFun𝐹 ∘
(Apply ∘ pprod( I , Bigcup ))) ↾ (V
× ran Succ))))𝑥 ∧
𝑥◡Apply〈𝑓, 𝑦〉) ↔ (𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
236 | 235 | exbidv 1928 |
. . . . . . . . . . . . . . . . . . 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 5031 |
. . . . . . . . . . . . . . . . . . . 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)))))) |
238 | 69 | elfix 33843 |
. . . . . . . . . . . . . . . . . . . 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)))))〈𝑓, 𝑦〉) |
239 | 69, 69 | brco 5713 |
. . . . . . . . . . . . . . . . . . . 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〈𝑓, 𝑦〉)) |
240 | 237, 238,
239 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . 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 6687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓‘𝑦) ∈ V |
242 | 241 | eqvinc 3545 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
243 | 236, 240,
242 | 3bitr4g 317 |
. . . . . . . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
244 | 243 | notbid 321 |
. . . . . . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
245 | 244 | 3expia 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
246 | 245 | pm5.32d 580 |
. . . . . . . . . . . . . . 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 407 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
248 | 246, 247 | bitrdi 290 |
. . . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
249 | 51, 248 | syl5bb 286 |
. . . . . . . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
250 | 249 | exbidv 1928 |
. . . . . . . . . . . 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 1833 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ¬
(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
252 | 250, 251 | bitr2di 291 |
. . . . . . . . . . 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))))))𝑦)) |
253 | 12 | eldm 5743 |
. . . . . . . . . . 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))))))𝑦) |
254 | 252, 253 | bitr4di 292 |
. . . . . . . . . 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)))))))) |
255 | 254 | con1bid 359 |
. . . . . . . . 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 3058 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
257 | 255, 256 | bitr4di 292 |
. . . . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
258 | 257 | pm5.32i 578 |
. . . . . . 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 472 |
. . . . . . 7
⊢ (((Fun
𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
260 | 258, 259 | bitri 278 |
. . . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
261 | 21, 37, 260 | 3bitri 300 |
. . . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
262 | 19, 20, 261 | 3bitr4ri 307 |
. . . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
263 | 262 | abbi2i 2871 |
. . 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
264 | 263 | unieqi 4809 |
. 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 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
265 | 1, 264 | eqtr4i 2764 |
1
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran
Succ))))))) |