Step |
Hyp |
Ref |
Expression |
1 |
|
inf3lem.1 |
⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) |
2 |
|
inf3lem.2 |
⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω ) |
3 |
|
inf3lem.3 |
⊢ 𝐴 ∈ V |
4 |
|
inf3lem.4 |
⊢ 𝐵 ∈ V |
5 |
1 2 3 4
|
inf3lemd |
⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ) |
6 |
1 2 3 4
|
inf3lem2 |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) ) |
7 |
6
|
com12 |
⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) ) |
8 |
|
pssdifn0 |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) → ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ ) |
9 |
5 7 8
|
syl6an |
⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ ) ) |
10 |
|
vex |
⊢ 𝑥 ∈ V |
11 |
10
|
difexi |
⊢ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∈ V |
12 |
|
zfreg |
⊢ ( ( ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∈ V ∧ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ ) → ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) |
13 |
11 12
|
mpan |
⊢ ( ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ → ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) |
14 |
|
eldifi |
⊢ ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) → 𝑣 ∈ 𝑥 ) |
15 |
|
inssdif0 |
⊢ ( ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) |
16 |
15
|
biimpri |
⊢ ( ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) |
17 |
14 16
|
anim12i |
⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) ) |
18 |
|
vex |
⊢ 𝑣 ∈ V |
19 |
|
fvex |
⊢ ( 𝐹 ‘ 𝐴 ) ∈ V |
20 |
1 2 18 19
|
inf3lema |
⊢ ( 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) ) |
21 |
17 20
|
sylibr |
⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) ) |
22 |
1 2 3 4
|
inf3lemc |
⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) ) |
23 |
22
|
eleq2d |
⊢ ( 𝐴 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ↔ 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ) |
24 |
21 23
|
syl5ibr |
⊢ ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ) ) |
25 |
|
eldifn |
⊢ ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) → ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) |
26 |
25
|
adantr |
⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) |
27 |
24 26
|
jca2 |
⊢ ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ) ) |
28 |
|
eleq2 |
⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ( 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ↔ 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ) ) |
29 |
28
|
biimprd |
⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) → 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ) |
30 |
|
iman |
⊢ ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) → 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ↔ ¬ ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ) |
31 |
29 30
|
sylib |
⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ¬ ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ) |
32 |
31
|
necon2ai |
⊢ ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) |
33 |
27 32
|
syl6 |
⊢ ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) |
34 |
33
|
expd |
⊢ ( 𝐴 ∈ ω → ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) → ( ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) ) |
35 |
34
|
rexlimdv |
⊢ ( 𝐴 ∈ ω → ( ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) |
36 |
13 35
|
syl5 |
⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) |
37 |
9 36
|
syldc |
⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) |