| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isf32lem.a |
⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 ) |
| 2 |
|
isf32lem.b |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) |
| 3 |
|
isf32lem.c |
⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) |
| 4 |
|
eldifi |
⊢ ( 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) → 𝑎 ∈ ( 𝐹 ‘ 𝐴 ) ) |
| 5 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → 𝐴 ∈ ω ) |
| 6 |
|
peano2 |
⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω ) |
| 7 |
6
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → suc 𝐵 ∈ ω ) |
| 8 |
|
nnord |
⊢ ( 𝐴 ∈ ω → Ord 𝐴 ) |
| 9 |
8
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → Ord 𝐴 ) |
| 10 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → 𝐵 ∈ 𝐴 ) |
| 11 |
|
ordsucss |
⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) ) |
| 12 |
9 10 11
|
sylc |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → suc 𝐵 ⊆ 𝐴 ) |
| 13 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → 𝜑 ) |
| 14 |
1 2 3
|
isf32lem1 |
⊢ ( ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ ( suc 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐵 ) ) |
| 15 |
5 7 12 13 14
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐵 ) ) |
| 16 |
15
|
sseld |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝑎 ∈ ( 𝐹 ‘ 𝐴 ) → 𝑎 ∈ ( 𝐹 ‘ suc 𝐵 ) ) ) |
| 17 |
|
elndif |
⊢ ( 𝑎 ∈ ( 𝐹 ‘ suc 𝐵 ) → ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) |
| 18 |
4 16 17
|
syl56 |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) → ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) ) |
| 19 |
18
|
ralrimiv |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ∀ 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) |
| 20 |
|
disj |
⊢ ( ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ ↔ ∀ 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) |
| 21 |
19 20
|
sylibr |
⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ ) |