Step |
Hyp |
Ref |
Expression |
1 |
|
dominf.1 |
⊢ 𝐴 ∈ V |
2 |
|
neeq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≠ ∅ ↔ 𝐴 ≠ ∅ ) ) |
3 |
|
id |
⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 ) |
4 |
|
unieq |
⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 ) |
5 |
3 4
|
sseq12d |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ 𝐴 ) ) |
6 |
2 5
|
anbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ∪ 𝐴 ) ) ) |
7 |
|
breq2 |
⊢ ( 𝑥 = 𝐴 → ( ω ≼ 𝑥 ↔ ω ≼ 𝐴 ) ) |
8 |
6 7
|
imbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ω ≼ 𝑥 ) ↔ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ∪ 𝐴 ) → ω ≼ 𝐴 ) ) ) |
9 |
|
eqid |
⊢ ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) |
10 |
|
eqid |
⊢ ( rec ( ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) |
11 |
9 10 1 1
|
inf3lem6 |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( rec ( ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) : ω –1-1→ 𝒫 𝑥 ) |
12 |
|
vpwex |
⊢ 𝒫 𝑥 ∈ V |
13 |
12
|
f1dom |
⊢ ( ( rec ( ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) : ω –1-1→ 𝒫 𝑥 → ω ≼ 𝒫 𝑥 ) |
14 |
|
pwfi |
⊢ ( 𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Fin ) |
15 |
14
|
biimpi |
⊢ ( 𝑥 ∈ Fin → 𝒫 𝑥 ∈ Fin ) |
16 |
|
isfinite |
⊢ ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω ) |
17 |
|
isfinite |
⊢ ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 𝑥 ≺ ω ) |
18 |
15 16 17
|
3imtr3i |
⊢ ( 𝑥 ≺ ω → 𝒫 𝑥 ≺ ω ) |
19 |
18
|
con3i |
⊢ ( ¬ 𝒫 𝑥 ≺ ω → ¬ 𝑥 ≺ ω ) |
20 |
12
|
domtriom |
⊢ ( ω ≼ 𝒫 𝑥 ↔ ¬ 𝒫 𝑥 ≺ ω ) |
21 |
|
vex |
⊢ 𝑥 ∈ V |
22 |
21
|
domtriom |
⊢ ( ω ≼ 𝑥 ↔ ¬ 𝑥 ≺ ω ) |
23 |
19 20 22
|
3imtr4i |
⊢ ( ω ≼ 𝒫 𝑥 → ω ≼ 𝑥 ) |
24 |
11 13 23
|
3syl |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ω ≼ 𝑥 ) |
25 |
1 8 24
|
vtocl |
⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ∪ 𝐴 ) → ω ≼ 𝐴 ) |