Proof of Theorem erdszelem1
Step | Hyp | Ref
| Expression |
1 | | ovex 7452 |
. . . 4
⊢
(1...𝐴) ∈
V |
2 | 1 | elpw2 5348 |
. . 3
⊢ (𝑋 ∈ 𝒫 (1...𝐴) ↔ 𝑋 ⊆ (1...𝐴)) |
3 | 2 | anbi1i 622 |
. 2
⊢ ((𝑋 ∈ 𝒫 (1...𝐴) ∧ ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋)) ↔ (𝑋 ⊆ (1...𝐴) ∧ ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))) |
4 | | reseq2 5980 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (𝐹 ↾ 𝑦) = (𝐹 ↾ 𝑋)) |
5 | | isoeq1 7324 |
. . . . . 6
⊢ ((𝐹 ↾ 𝑦) = (𝐹 ↾ 𝑋) → ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ↔ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)))) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ↔ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)))) |
7 | | isoeq4 7327 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ↔ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑦)))) |
8 | | imaeq2 6060 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (𝐹 “ 𝑦) = (𝐹 “ 𝑋)) |
9 | | isoeq5 7328 |
. . . . . 6
⊢ ((𝐹 “ 𝑦) = (𝐹 “ 𝑋) → ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑦)) ↔ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)))) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑦)) ↔ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)))) |
11 | 6, 7, 10 | 3bitrd 304 |
. . . 4
⊢ (𝑦 = 𝑋 → ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ↔ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)))) |
12 | | eleq2 2814 |
. . . 4
⊢ (𝑦 = 𝑋 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑋)) |
13 | 11, 12 | anbi12d 630 |
. . 3
⊢ (𝑦 = 𝑋 → (((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦) ↔ ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))) |
14 | | erdszelem1.1 |
. . 3
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} |
15 | 13, 14 | elrab2 3682 |
. 2
⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝒫 (1...𝐴) ∧ ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))) |
16 | | 3anass 1092 |
. 2
⊢ ((𝑋 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋) ↔ (𝑋 ⊆ (1...𝐴) ∧ ((𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))) |
17 | 3, 15, 16 | 3bitr4i 302 |
1
⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋)) |