Step |
Hyp |
Ref |
Expression |
1 |
|
inf3lem.1 |
⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) |
2 |
|
inf3lem.2 |
⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω ) |
3 |
|
inf3lem.3 |
⊢ 𝐴 ∈ V |
4 |
|
inf3lem.4 |
⊢ 𝐵 ∈ V |
5 |
|
fveq2 |
⊢ ( 𝐴 = ∅ → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ∅ ) ) |
6 |
1 2 3 4
|
inf3lemb |
⊢ ( 𝐹 ‘ ∅ ) = ∅ |
7 |
5 6
|
eqtrdi |
⊢ ( 𝐴 = ∅ → ( 𝐹 ‘ 𝐴 ) = ∅ ) |
8 |
|
0ss |
⊢ ∅ ⊆ 𝑥 |
9 |
7 8
|
eqsstrdi |
⊢ ( 𝐴 = ∅ → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) |
10 |
9
|
a1d |
⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) ) |
11 |
|
nnsuc |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑣 ∈ ω 𝐴 = suc 𝑣 ) |
12 |
|
vex |
⊢ 𝑣 ∈ V |
13 |
1 2 12 4
|
inf3lemc |
⊢ ( 𝑣 ∈ ω → ( 𝐹 ‘ suc 𝑣 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑣 ) ) ) |
14 |
13
|
eleq2d |
⊢ ( 𝑣 ∈ ω → ( 𝑢 ∈ ( 𝐹 ‘ suc 𝑣 ) ↔ 𝑢 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑣 ) ) ) ) |
15 |
|
vex |
⊢ 𝑢 ∈ V |
16 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑣 ) ∈ V |
17 |
1 2 15 16
|
inf3lema |
⊢ ( 𝑢 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑣 ) ) ↔ ( 𝑢 ∈ 𝑥 ∧ ( 𝑢 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑣 ) ) ) |
18 |
17
|
simplbi |
⊢ ( 𝑢 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑣 ) ) → 𝑢 ∈ 𝑥 ) |
19 |
14 18
|
syl6bi |
⊢ ( 𝑣 ∈ ω → ( 𝑢 ∈ ( 𝐹 ‘ suc 𝑣 ) → 𝑢 ∈ 𝑥 ) ) |
20 |
19
|
ssrdv |
⊢ ( 𝑣 ∈ ω → ( 𝐹 ‘ suc 𝑣 ) ⊆ 𝑥 ) |
21 |
|
fveq2 |
⊢ ( 𝐴 = suc 𝑣 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝑣 ) ) |
22 |
21
|
sseq1d |
⊢ ( 𝐴 = suc 𝑣 → ( ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ↔ ( 𝐹 ‘ suc 𝑣 ) ⊆ 𝑥 ) ) |
23 |
20 22
|
syl5ibrcom |
⊢ ( 𝑣 ∈ ω → ( 𝐴 = suc 𝑣 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) ) |
24 |
23
|
rexlimiv |
⊢ ( ∃ 𝑣 ∈ ω 𝐴 = suc 𝑣 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) |
25 |
11 24
|
syl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) |
26 |
25
|
expcom |
⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) ) |
27 |
10 26
|
pm2.61ine |
⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) |