Step |
Hyp |
Ref |
Expression |
1 |
|
inf3lem.1 |
⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) |
2 |
|
inf3lem.2 |
⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω ) |
3 |
|
inf3lem.3 |
⊢ 𝐴 ∈ V |
4 |
|
inf3lem.4 |
⊢ 𝐵 ∈ V |
5 |
|
elnn |
⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐴 ∈ ω ) → 𝐵 ∈ ω ) |
6 |
5
|
ancoms |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ω ) |
7 |
|
nnord |
⊢ ( 𝐴 ∈ ω → Ord 𝐴 ) |
8 |
|
ordsucss |
⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) ) |
9 |
7 8
|
syl |
⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) ) |
11 |
|
peano2b |
⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω ) |
12 |
|
fveq2 |
⊢ ( 𝑣 = suc 𝐵 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝐵 ) ) |
13 |
12
|
psseq2d |
⊢ ( 𝑣 = suc 𝐵 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) |
14 |
13
|
imbi2d |
⊢ ( 𝑣 = suc 𝐵 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) ) |
15 |
|
fveq2 |
⊢ ( 𝑣 = 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) ) |
16 |
15
|
psseq2d |
⊢ ( 𝑣 = 𝑢 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) ) |
17 |
16
|
imbi2d |
⊢ ( 𝑣 = 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) ) ) |
18 |
|
fveq2 |
⊢ ( 𝑣 = suc 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝑢 ) ) |
19 |
18
|
psseq2d |
⊢ ( 𝑣 = suc 𝑢 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) |
20 |
19
|
imbi2d |
⊢ ( 𝑣 = suc 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) ) |
21 |
|
fveq2 |
⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) |
22 |
21
|
psseq2d |
⊢ ( 𝑣 = 𝐴 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) |
23 |
22
|
imbi2d |
⊢ ( 𝑣 = 𝐴 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) ) |
24 |
1 2 4 4
|
inf3lem4 |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐵 ∈ ω → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) |
25 |
24
|
com12 |
⊢ ( 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) |
26 |
11 25
|
sylbir |
⊢ ( suc 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) |
27 |
|
vex |
⊢ 𝑢 ∈ V |
28 |
1 2 27 4
|
inf3lem4 |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑢 ∈ ω → ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) |
29 |
|
psstr |
⊢ ( ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) |
30 |
29
|
expcom |
⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) |
31 |
28 30
|
syl6com |
⊢ ( 𝑢 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) ) |
32 |
31
|
a2d |
⊢ ( 𝑢 ∈ ω → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) ) |
33 |
32
|
ad2antrr |
⊢ ( ( ( 𝑢 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ suc 𝐵 ⊆ 𝑢 ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) ) |
34 |
14 17 20 23 26 33
|
findsg |
⊢ ( ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ suc 𝐵 ⊆ 𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) |
35 |
34
|
ex |
⊢ ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) → ( suc 𝐵 ⊆ 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) ) |
36 |
11 35
|
sylan2b |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐵 ⊆ 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) ) |
37 |
10 36
|
syld |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) ) |
38 |
37
|
impancom |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) ) |
39 |
6 38
|
mpd |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) |
40 |
39
|
com12 |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) |