Proof of Theorem oaordex
| Step | Hyp | Ref
| Expression |
| 1 | | onelss 6426 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
| 2 | 1 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵)) |
| 3 | | oawordex 8595 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)) |
| 4 | 2, 3 | sylibd 239 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)) |
| 5 | | oaord1 8589 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅
∈ 𝑥 ↔ 𝐴 ∈ (𝐴 +o 𝑥))) |
| 6 | | eleq2 2830 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +o 𝑥) = 𝐵 → (𝐴 ∈ (𝐴 +o 𝑥) ↔ 𝐴 ∈ 𝐵)) |
| 7 | 5, 6 | sylan9bb 509 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ (𝐴 +o 𝑥) = 𝐵) → (∅ ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) |
| 8 | 7 | biimprcd 250 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝐵 → (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ (𝐴 +o 𝑥) = 𝐵) → ∅ ∈ 𝑥)) |
| 9 | 8 | exp4c 432 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On → (𝑥 ∈ On → ((𝐴 +o 𝑥) = 𝐵 → ∅ ∈ 𝑥)))) |
| 10 | 9 | com12 32 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐴 ∈ 𝐵 → (𝑥 ∈ On → ((𝐴 +o 𝑥) = 𝐵 → ∅ ∈ 𝑥)))) |
| 11 | 10 | imp4b 421 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐴 ∈ 𝐵) → ((𝑥 ∈ On ∧ (𝐴 +o 𝑥) = 𝐵) → ∅ ∈ 𝑥)) |
| 12 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ (𝐴 +o 𝑥) = 𝐵) → (𝐴 +o 𝑥) = 𝐵) |
| 13 | 11, 12 | jca2 513 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐴 ∈ 𝐵) → ((𝑥 ∈ On ∧ (𝐴 +o 𝑥) = 𝐵) → (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
| 14 | 13 | expd 415 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝑥 ∈ On → ((𝐴 +o 𝑥) = 𝐵 → (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
| 15 | 14 | reximdvai 3165 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐴 ∈ 𝐵) → (∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
| 16 | 15 | ex 412 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 ∈ 𝐵 → (∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
| 17 | 16 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 → (∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵 → ∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))) |
| 18 | 4, 17 | mpdd 43 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
| 19 | 7 | biimpd 229 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ (𝐴 +o 𝑥) = 𝐵) → (∅ ∈ 𝑥 → 𝐴 ∈ 𝐵)) |
| 20 | 19 | exp31 419 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝑥 ∈ On → ((𝐴 +o 𝑥) = 𝐵 → (∅ ∈ 𝑥 → 𝐴 ∈ 𝐵)))) |
| 21 | 20 | com34 91 |
. . . . 5
⊢ (𝐴 ∈ On → (𝑥 ∈ On → (∅
∈ 𝑥 → ((𝐴 +o 𝑥) = 𝐵 → 𝐴 ∈ 𝐵)))) |
| 22 | 21 | imp4a 422 |
. . . 4
⊢ (𝐴 ∈ On → (𝑥 ∈ On → ((∅
∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵))) |
| 23 | 22 | rexlimdv 3153 |
. . 3
⊢ (𝐴 ∈ On → (∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
| 24 | 23 | adantr 480 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵) → 𝐴 ∈ 𝐵)) |
| 25 | 18, 24 | impbid 212 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ On (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |