| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dfrdg3 |
⊢ rec ( 𝐹 , 𝐴 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } |
| 2 |
|
an12 |
⊢ ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 3 |
|
df-fn |
⊢ ( 𝑓 Fn 𝑥 ↔ ( Fun 𝑓 ∧ dom 𝑓 = 𝑥 ) ) |
| 4 |
|
ancom |
⊢ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝑥 ) ↔ ( dom 𝑓 = 𝑥 ∧ Fun 𝑓 ) ) |
| 5 |
|
eqcom |
⊢ ( dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓 ) |
| 6 |
5
|
anbi1i |
⊢ ( ( dom 𝑓 = 𝑥 ∧ Fun 𝑓 ) ↔ ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ) |
| 7 |
3 4 6
|
3bitri |
⊢ ( 𝑓 Fn 𝑥 ↔ ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ) |
| 8 |
7
|
anbi1i |
⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 9 |
|
anass |
⊢ ( ( ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) ) |
| 10 |
2 8 9
|
3bitri |
⊢ ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) ) |
| 11 |
10
|
exbii |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) ) |
| 12 |
|
vex |
⊢ 𝑓 ∈ V |
| 13 |
12
|
dmex |
⊢ dom 𝑓 ∈ V |
| 14 |
|
eleq1 |
⊢ ( 𝑥 = dom 𝑓 → ( 𝑥 ∈ On ↔ dom 𝑓 ∈ On ) ) |
| 15 |
|
raleq |
⊢ ( 𝑥 = dom 𝑓 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 16 |
14 15
|
anbi12d |
⊢ ( 𝑥 = dom 𝑓 → ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 17 |
16
|
anbi2d |
⊢ ( 𝑥 = dom 𝑓 → ( ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) ) |
| 18 |
13 17
|
ceqsexv |
⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 19 |
11 18
|
bitri |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 20 |
|
df-rex |
⊢ ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 21 |
|
eldif |
⊢ ( 𝑓 ∈ ( ( 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 |
⊢ ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ↔ ( 𝑓 ∈ Funs ∧ 𝑓 ∈ ( ◡ Domain “ On ) ) ) |
| 23 |
12
|
elfuns |
⊢ ( 𝑓 ∈ Funs ↔ Fun 𝑓 ) |
| 24 |
12
|
elima |
⊢ ( 𝑓 ∈ ( ◡ Domain “ On ) ↔ ∃ 𝑥 ∈ On 𝑥 ◡ Domain 𝑓 ) |
| 25 |
|
df-rex |
⊢ ( ∃ 𝑥 ∈ On 𝑥 ◡ Domain 𝑓 ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ 𝑥 ◡ Domain 𝑓 ) ) |
| 26 |
|
vex |
⊢ 𝑥 ∈ V |
| 27 |
26 12
|
brcnv |
⊢ ( 𝑥 ◡ Domain 𝑓 ↔ 𝑓 Domain 𝑥 ) |
| 28 |
12 26
|
brdomain |
⊢ ( 𝑓 Domain 𝑥 ↔ 𝑥 = dom 𝑓 ) |
| 29 |
27 28
|
bitri |
⊢ ( 𝑥 ◡ Domain 𝑓 ↔ 𝑥 = dom 𝑓 ) |
| 30 |
29
|
anbi1ci |
⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ◡ Domain 𝑓 ) ↔ ( 𝑥 = dom 𝑓 ∧ 𝑥 ∈ On ) ) |
| 31 |
30
|
exbii |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ 𝑥 ◡ Domain 𝑓 ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ∈ On ) ) |
| 32 |
13 14
|
ceqsexv |
⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ∈ On ) ↔ dom 𝑓 ∈ On ) |
| 33 |
31 32
|
bitri |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ 𝑥 ◡ Domain 𝑓 ) ↔ dom 𝑓 ∈ On ) |
| 34 |
24 25 33
|
3bitri |
⊢ ( 𝑓 ∈ ( ◡ Domain “ On ) ↔ dom 𝑓 ∈ On ) |
| 35 |
23 34
|
anbi12i |
⊢ ( ( 𝑓 ∈ Funs ∧ 𝑓 ∈ ( ◡ Domain “ On ) ) ↔ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) |
| 36 |
22 35
|
bitri |
⊢ ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ↔ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ) |
| 37 |
36
|
anbi1i |
⊢ ( ( 𝑓 ∈ ( 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 |
⊢ ( 𝑓 ( ( ◡ 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 |
⊢ 𝑦 ∈ V |
| 40 |
12 39
|
brco |
⊢ ( 𝑓 ( ◡ E ∘ Domain ) 𝑦 ↔ ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ) |
| 41 |
28
|
anbi1i |
⊢ ( ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ↔ ( 𝑥 = dom 𝑓 ∧ 𝑥 ◡ E 𝑦 ) ) |
| 42 |
41
|
exbii |
⊢ ( ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ◡ E 𝑦 ) ) |
| 43 |
|
breq1 |
⊢ ( 𝑥 = dom 𝑓 → ( 𝑥 ◡ E 𝑦 ↔ dom 𝑓 ◡ E 𝑦 ) ) |
| 44 |
13 43
|
ceqsexv |
⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ◡ E 𝑦 ) ↔ dom 𝑓 ◡ E 𝑦 ) |
| 45 |
42 44
|
bitri |
⊢ ( ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ↔ dom 𝑓 ◡ E 𝑦 ) |
| 46 |
13 39
|
brcnv |
⊢ ( dom 𝑓 ◡ E 𝑦 ↔ 𝑦 E dom 𝑓 ) |
| 47 |
13
|
epeli |
⊢ ( 𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓 ) |
| 48 |
46 47
|
bitri |
⊢ ( dom 𝑓 ◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓 ) |
| 49 |
40 45 48
|
3bitri |
⊢ ( 𝑓 ( ◡ E ∘ Domain ) 𝑦 ↔ 𝑦 ∈ dom 𝑓 ) |
| 50 |
49
|
anbi1i |
⊢ ( ( 𝑓 ( ◡ 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 |
⊢ ( 𝑓 ( ( ◡ 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 |
⊢ ( ( dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓 ) → 𝑦 ∈ On ) |
| 53 |
52
|
3adant1 |
⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓 ) → 𝑦 ∈ On ) |
| 54 |
|
brun |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( 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 |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) 𝑥 ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ∧ 𝑥 ∈ { ∪ { 𝐴 } } ) ) |
| 56 |
|
opelxp |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ↔ ( 𝑓 ∈ V ∧ 𝑦 ∈ { ∅ } ) ) |
| 57 |
12 56
|
mpbiran |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ↔ 𝑦 ∈ { ∅ } ) |
| 58 |
|
velsn |
⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ ) |
| 59 |
57 58
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ↔ 𝑦 = ∅ ) |
| 60 |
|
velsn |
⊢ ( 𝑥 ∈ { ∪ { 𝐴 } } ↔ 𝑥 = ∪ { 𝐴 } ) |
| 61 |
59 60
|
anbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ∧ 𝑥 ∈ { ∪ { 𝐴 } } ) ↔ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) |
| 62 |
55 61
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) 𝑥 ↔ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) |
| 63 |
|
brun |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( 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 |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) 𝑥 ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ) ) |
| 65 |
|
opelxp |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ↔ ( 𝑓 ∈ V ∧ 𝑦 ∈ Limits ) ) |
| 66 |
12 65
|
mpbiran |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ↔ 𝑦 ∈ Limits ) |
| 67 |
39
|
ellimits |
⊢ ( 𝑦 ∈ Limits ↔ Lim 𝑦 ) |
| 68 |
66 67
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ↔ Lim 𝑦 ) |
| 69 |
|
opex |
⊢ ⟨ 𝑓 , 𝑦 ⟩ ∈ V |
| 70 |
69 26
|
brco |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ↔ ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ∧ 𝑧 Bigcup 𝑥 ) ) |
| 71 |
|
vex |
⊢ 𝑧 ∈ V |
| 72 |
12 39 71
|
brimg |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ↔ 𝑧 = ( 𝑓 “ 𝑦 ) ) |
| 73 |
26
|
brbigcup |
⊢ ( 𝑧 Bigcup 𝑥 ↔ ∪ 𝑧 = 𝑥 ) |
| 74 |
72 73
|
anbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ∧ 𝑧 Bigcup 𝑥 ) ↔ ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) ) |
| 75 |
74
|
exbii |
⊢ ( ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ∧ 𝑧 Bigcup 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) ) |
| 76 |
12
|
imaex |
⊢ ( 𝑓 “ 𝑦 ) ∈ V |
| 77 |
|
unieq |
⊢ ( 𝑧 = ( 𝑓 “ 𝑦 ) → ∪ 𝑧 = ∪ ( 𝑓 “ 𝑦 ) ) |
| 78 |
77
|
eqeq1d |
⊢ ( 𝑧 = ( 𝑓 “ 𝑦 ) → ( ∪ 𝑧 = 𝑥 ↔ ∪ ( 𝑓 “ 𝑦 ) = 𝑥 ) ) |
| 79 |
76 78
|
ceqsexv |
⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) ↔ ∪ ( 𝑓 “ 𝑦 ) = 𝑥 ) |
| 80 |
|
eqcom |
⊢ ( ∪ ( 𝑓 “ 𝑦 ) = 𝑥 ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) |
| 81 |
79 80
|
bitri |
⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) |
| 82 |
70 75 81
|
3bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) |
| 83 |
68 82
|
anbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ) ↔ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) |
| 84 |
64 83
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) 𝑥 ↔ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) |
| 85 |
26
|
brresi |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) 𝑥 ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ) ) |
| 86 |
|
opelxp |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ↔ ( 𝑓 ∈ V ∧ 𝑦 ∈ ran Succ ) ) |
| 87 |
12 86
|
mpbiran |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ↔ 𝑦 ∈ ran Succ ) |
| 88 |
39
|
elrn |
⊢ ( 𝑦 ∈ ran Succ ↔ ∃ 𝑧 𝑧 Succ 𝑦 ) |
| 89 |
71 39
|
brsuccf |
⊢ ( 𝑧 Succ 𝑦 ↔ 𝑦 = suc 𝑧 ) |
| 90 |
89
|
exbii |
⊢ ( ∃ 𝑧 𝑧 Succ 𝑦 ↔ ∃ 𝑧 𝑦 = suc 𝑧 ) |
| 91 |
87 88 90
|
3bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ↔ ∃ 𝑧 𝑦 = suc 𝑧 ) |
| 92 |
69 26
|
brco |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ↔ ∃ 𝑎 ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ∧ 𝑎 FullFun 𝐹 𝑥 ) ) |
| 93 |
|
vex |
⊢ 𝑎 ∈ V |
| 94 |
69 93
|
brco |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ↔ ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ∧ 𝑧 Apply 𝑎 ) ) |
| 95 |
12 39 71
|
brpprod3a |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ) |
| 96 |
|
3anrot |
⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ↔ ( 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ) |
| 97 |
93
|
ideq |
⊢ ( 𝑓 I 𝑎 ↔ 𝑓 = 𝑎 ) |
| 98 |
|
equcom |
⊢ ( 𝑓 = 𝑎 ↔ 𝑎 = 𝑓 ) |
| 99 |
97 98
|
bitri |
⊢ ( 𝑓 I 𝑎 ↔ 𝑎 = 𝑓 ) |
| 100 |
|
vex |
⊢ 𝑏 ∈ V |
| 101 |
100
|
brbigcup |
⊢ ( 𝑦 Bigcup 𝑏 ↔ ∪ 𝑦 = 𝑏 ) |
| 102 |
|
eqcom |
⊢ ( ∪ 𝑦 = 𝑏 ↔ 𝑏 = ∪ 𝑦 ) |
| 103 |
101 102
|
bitri |
⊢ ( 𝑦 Bigcup 𝑏 ↔ 𝑏 = ∪ 𝑦 ) |
| 104 |
|
biid |
⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) |
| 105 |
99 103 104
|
3anbi123i |
⊢ ( ( 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ) |
| 106 |
96 105
|
bitri |
⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ↔ ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ) |
| 107 |
106
|
2exbii |
⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ) |
| 108 |
|
vuniex |
⊢ ∪ 𝑦 ∈ V |
| 109 |
|
opeq1 |
⊢ ( 𝑎 = 𝑓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑓 , 𝑏 ⟩ ) |
| 110 |
109
|
eqeq2d |
⊢ ( 𝑎 = 𝑓 → ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑓 , 𝑏 ⟩ ) ) |
| 111 |
|
opeq2 |
⊢ ( 𝑏 = ∪ 𝑦 → ⟨ 𝑓 , 𝑏 ⟩ = ⟨ 𝑓 , ∪ 𝑦 ⟩ ) |
| 112 |
111
|
eqeq2d |
⊢ ( 𝑏 = ∪ 𝑦 → ( 𝑧 = ⟨ 𝑓 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ) ) |
| 113 |
12 108 110 112
|
ceqsex2v |
⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ) |
| 114 |
95 107 113
|
3bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ↔ 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ) |
| 115 |
114
|
anbi1i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ∧ 𝑧 Apply 𝑎 ) ↔ ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) ) |
| 116 |
115
|
exbii |
⊢ ( ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ∧ 𝑧 Apply 𝑎 ) ↔ ∃ 𝑧 ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) ) |
| 117 |
|
opex |
⊢ ⟨ 𝑓 , ∪ 𝑦 ⟩ ∈ V |
| 118 |
|
breq1 |
⊢ ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ → ( 𝑧 Apply 𝑎 ↔ ⟨ 𝑓 , ∪ 𝑦 ⟩ Apply 𝑎 ) ) |
| 119 |
117 118
|
ceqsexv |
⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) ↔ ⟨ 𝑓 , ∪ 𝑦 ⟩ Apply 𝑎 ) |
| 120 |
12 108 93
|
brapply |
⊢ ( ⟨ 𝑓 , ∪ 𝑦 ⟩ Apply 𝑎 ↔ 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ) |
| 121 |
119 120
|
bitri |
⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) ↔ 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ) |
| 122 |
94 116 121
|
3bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ↔ 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ) |
| 123 |
93 26
|
brfullfun |
⊢ ( 𝑎 FullFun 𝐹 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) |
| 124 |
122 123
|
anbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ∧ 𝑎 FullFun 𝐹 𝑥 ) ↔ ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) ) |
| 125 |
124
|
exbii |
⊢ ( ∃ 𝑎 ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ∧ 𝑎 FullFun 𝐹 𝑥 ) ↔ ∃ 𝑎 ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) ) |
| 126 |
|
fvex |
⊢ ( 𝑓 ‘ ∪ 𝑦 ) ∈ V |
| 127 |
|
fveq2 |
⊢ ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) |
| 128 |
127
|
eqeq2d |
⊢ ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) → ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 129 |
126 128
|
ceqsexv |
⊢ ( ∃ 𝑎 ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) |
| 130 |
92 125 129
|
3bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) |
| 131 |
91 130
|
anbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ) ↔ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 132 |
85 131
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) 𝑥 ↔ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 133 |
84 132
|
orbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) 𝑥 ∨ ⟨ 𝑓 , 𝑦 ⟩ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) 𝑥 ) ↔ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 134 |
63 133
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) 𝑥 ↔ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 135 |
62 134
|
orbi12i |
⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) 𝑥 ∨ ⟨ 𝑓 , 𝑦 ⟩ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) 𝑥 ) ↔ ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 136 |
54 135
|
bitri |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) ∪ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) ) 𝑥 ↔ ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 137 |
|
onzsl |
⊢ ( 𝑦 ∈ On ↔ ( 𝑦 = ∅ ∨ ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 ∨ ( 𝑦 ∈ V ∧ Lim 𝑦 ) ) ) |
| 138 |
|
nlim0 |
⊢ ¬ Lim ∅ |
| 139 |
|
limeq |
⊢ ( 𝑦 = ∅ → ( Lim 𝑦 ↔ Lim ∅ ) ) |
| 140 |
138 139
|
mtbiri |
⊢ ( 𝑦 = ∅ → ¬ Lim 𝑦 ) |
| 141 |
140
|
intnanrd |
⊢ ( 𝑦 = ∅ → ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) |
| 142 |
|
nsuceq0 |
⊢ suc 𝑧 ≠ ∅ |
| 143 |
|
neeq2 |
⊢ ( 𝑦 = ∅ → ( suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅ ) ) |
| 144 |
142 143
|
mpbiri |
⊢ ( 𝑦 = ∅ → suc 𝑧 ≠ 𝑦 ) |
| 145 |
144
|
necomd |
⊢ ( 𝑦 = ∅ → 𝑦 ≠ suc 𝑧 ) |
| 146 |
145
|
neneqd |
⊢ ( 𝑦 = ∅ → ¬ 𝑦 = suc 𝑧 ) |
| 147 |
146
|
nexdv |
⊢ ( 𝑦 = ∅ → ¬ ∃ 𝑧 𝑦 = suc 𝑧 ) |
| 148 |
147
|
intnanrd |
⊢ ( 𝑦 = ∅ → ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 149 |
|
ioran |
⊢ ( ¬ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ( ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∧ ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 150 |
141 148 149
|
sylanbrc |
⊢ ( 𝑦 = ∅ → ¬ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 151 |
|
orel2 |
⊢ ( ¬ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) ) |
| 152 |
150 151
|
syl |
⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) ) |
| 153 |
|
iftrue |
⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( 𝐴 ∈ V , 𝐴 , ∅ ) ) |
| 154 |
|
unisnif |
⊢ ∪ { 𝐴 } = if ( 𝐴 ∈ V , 𝐴 , ∅ ) |
| 155 |
153 154
|
eqtr4di |
⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ∪ { 𝐴 } ) |
| 156 |
155
|
eqeq2d |
⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ 𝑥 = ∪ { 𝐴 } ) ) |
| 157 |
156
|
biimprd |
⊢ ( 𝑦 = ∅ → ( 𝑥 = ∪ { 𝐴 } → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 158 |
157
|
adantld |
⊢ ( 𝑦 = ∅ → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 159 |
152 158
|
syld |
⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 160 |
156
|
biimpd |
⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → 𝑥 = ∪ { 𝐴 } ) ) |
| 161 |
160
|
anc2li |
⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) ) |
| 162 |
|
orc |
⊢ ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 163 |
161 162
|
syl6 |
⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 164 |
159 163
|
impbid |
⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 165 |
|
neeq1 |
⊢ ( 𝑦 = suc 𝑧 → ( 𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅ ) ) |
| 166 |
142 165
|
mpbiri |
⊢ ( 𝑦 = suc 𝑧 → 𝑦 ≠ ∅ ) |
| 167 |
166
|
neneqd |
⊢ ( 𝑦 = suc 𝑧 → ¬ 𝑦 = ∅ ) |
| 168 |
167
|
intnanrd |
⊢ ( 𝑦 = suc 𝑧 → ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) |
| 169 |
168
|
rexlimivw |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) |
| 170 |
|
orel1 |
⊢ ( ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 171 |
169 170
|
syl |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 172 |
|
nlimsucg |
⊢ ( 𝑧 ∈ V → ¬ Lim suc 𝑧 ) |
| 173 |
172
|
elv |
⊢ ¬ Lim suc 𝑧 |
| 174 |
|
limeq |
⊢ ( 𝑦 = suc 𝑧 → ( Lim 𝑦 ↔ Lim suc 𝑧 ) ) |
| 175 |
173 174
|
mtbiri |
⊢ ( 𝑦 = suc 𝑧 → ¬ Lim 𝑦 ) |
| 176 |
175
|
rexlimivw |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦 ) |
| 177 |
176
|
intnanrd |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) |
| 178 |
|
orel1 |
⊢ ( ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 179 |
177 178
|
syl |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 180 |
142
|
neii |
⊢ ¬ suc 𝑧 = ∅ |
| 181 |
180
|
iffalsei |
⊢ if ( suc 𝑧 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) |
| 182 |
|
iffalse |
⊢ ( ¬ Lim suc 𝑧 → if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) |
| 183 |
71 172 182
|
mp2b |
⊢ if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) |
| 184 |
181 183
|
eqtri |
⊢ if ( suc 𝑧 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) |
| 185 |
|
eqeq1 |
⊢ ( 𝑦 = suc 𝑧 → ( 𝑦 = ∅ ↔ suc 𝑧 = ∅ ) ) |
| 186 |
|
unieq |
⊢ ( 𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧 ) |
| 187 |
186
|
fveq2d |
⊢ ( 𝑦 = suc 𝑧 → ( 𝑓 ‘ ∪ 𝑦 ) = ( 𝑓 ‘ ∪ suc 𝑧 ) ) |
| 188 |
187
|
fveq2d |
⊢ ( 𝑦 = suc 𝑧 → ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) |
| 189 |
174 188
|
ifbieq2d |
⊢ ( 𝑦 = suc 𝑧 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) |
| 190 |
185 189
|
ifbieq2d |
⊢ ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( suc 𝑧 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) ) |
| 191 |
184 190 188
|
3eqtr4a |
⊢ ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) |
| 192 |
191
|
rexlimivw |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) |
| 193 |
192
|
eqeq2d |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 194 |
193
|
biimprd |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 195 |
194
|
adantld |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 196 |
171 179 195
|
3syld |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 197 |
|
rexex |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ∃ 𝑧 𝑦 = suc 𝑧 ) |
| 198 |
193
|
biimpd |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 199 |
|
olc |
⊢ ( ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 200 |
199
|
olcd |
⊢ ( ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 201 |
197 198 200
|
syl6an |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 202 |
196 201
|
impbid |
⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 203 |
140
|
con2i |
⊢ ( Lim 𝑦 → ¬ 𝑦 = ∅ ) |
| 204 |
203
|
intnanrd |
⊢ ( Lim 𝑦 → ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) |
| 205 |
204 170
|
syl |
⊢ ( Lim 𝑦 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 206 |
175
|
exlimiv |
⊢ ( ∃ 𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦 ) |
| 207 |
206
|
con2i |
⊢ ( Lim 𝑦 → ¬ ∃ 𝑧 𝑦 = suc 𝑧 ) |
| 208 |
207
|
intnanrd |
⊢ ( Lim 𝑦 → ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 209 |
|
orel2 |
⊢ ( ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) ) |
| 210 |
208 209
|
syl |
⊢ ( Lim 𝑦 → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) ) |
| 211 |
203
|
iffalsed |
⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) |
| 212 |
|
iftrue |
⊢ ( Lim 𝑦 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) = ∪ ( 𝑓 “ 𝑦 ) ) |
| 213 |
211 212
|
eqtrd |
⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ∪ ( 𝑓 “ 𝑦 ) ) |
| 214 |
213
|
eqeq2d |
⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) |
| 215 |
214
|
biimprd |
⊢ ( Lim 𝑦 → ( 𝑥 = ∪ ( 𝑓 “ 𝑦 ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 216 |
215
|
adantld |
⊢ ( Lim 𝑦 → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 217 |
205 210 216
|
3syld |
⊢ ( Lim 𝑦 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 218 |
217
|
adantl |
⊢ ( ( 𝑦 ∈ V ∧ Lim 𝑦 ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 219 |
214
|
biimpd |
⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) |
| 220 |
219
|
anc2li |
⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) ) |
| 221 |
|
orc |
⊢ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) |
| 222 |
221
|
olcd |
⊢ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 223 |
220 222
|
syl6 |
⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 224 |
223
|
adantl |
⊢ ( ( 𝑦 ∈ V ∧ Lim 𝑦 ) → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 225 |
218 224
|
impbid |
⊢ ( ( 𝑦 ∈ V ∧ Lim 𝑦 ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 226 |
164 202 225
|
3jaoi |
⊢ ( ( 𝑦 = ∅ ∨ ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 ∨ ( 𝑦 ∈ V ∧ Lim 𝑦 ) ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 227 |
137 226
|
sylbi |
⊢ ( 𝑦 ∈ On → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 228 |
136 227
|
bitrid |
⊢ ( 𝑦 ∈ On → ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) ∪ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) ) 𝑥 ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 229 |
53 228
|
syl |
⊢ ( ( 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 |
⊢ ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ ⟨ 𝑓 , 𝑦 ⟩ Apply 𝑥 ) |
| 231 |
12 39 26
|
brapply |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ Apply 𝑥 ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) ) |
| 232 |
230 231
|
bitri |
⊢ ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) ) |
| 233 |
232
|
a1i |
⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) ) ) |
| 234 |
229 233
|
anbi12d |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( 𝑓 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 |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ 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 |
⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ◡ 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 |
⊢ ( 𝑓 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 |
⊢ ( 𝑓 ‘ 𝑦 ) ∈ V |
| 242 |
241
|
eqvinc |
⊢ ( ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ∧ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 243 |
236 240 242
|
3bitr4g |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ¬ ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 248 |
246 247
|
bitrdi |
⊢ ( ( 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
|
bitrid |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ∃ 𝑦 ¬ ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ¬ ∀ 𝑦 ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 252 |
250 251
|
bitr2di |
⊢ ( ( 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 |
⊢ ( 𝑓 ∈ 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) |
| 257 |
255 256
|
bitr4di |
⊢ ( ( 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 |
⊢ ( ( ( 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 |
⊢ ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) |
| 260 |
258 259
|
bitri |
⊢ ( ( ( 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 |
⊢ ( 𝑓 ∈ ( ( 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 |
⊢ ( 𝑓 ∈ ( ( 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
|
eqabi |
⊢ ( ( 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 |
⊢ ∪ ( ( 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 |
⊢ rec ( 𝐹 , 𝐴 ) = ∪ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) ∪ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) ) ) ) ) |