Proof of Theorem oadif1lem
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ∈ On) |
| 2 | | oadif1lem.cl1 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊕ 𝐵) ∈ On) |
| 3 | | onelon 6409 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊕ 𝐵) ∈ On ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵)) → 𝑦 ∈ On) |
| 4 | 2, 3 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵)) → 𝑦 ∈ On) |
| 5 | | ontri1 6418 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴)) |
| 6 | 1, 4, 5 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵)) → (𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴)) |
| 7 | 6 | pm5.32da 579 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ 𝐴 ⊆ 𝑦) ↔ (𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))) |
| 8 | | ancom 460 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ 𝐴 ⊆ 𝑦) ↔ (𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵))) |
| 9 | 7, 8 | bitr3di 286 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) ↔ (𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵)))) |
| 10 | | oadif1lem.sub |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵))) → ∃𝑏 ∈ 𝐵 (𝐴 ⊕ 𝑏) = 𝑦) |
| 11 | 9, 10 | sylbida 592 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) → ∃𝑏 ∈ 𝐵 (𝐴 ⊕ 𝑏) = 𝑦) |
| 12 | | eqcom 2744 |
. . . . . . 7
⊢ ((𝐴 ⊕ 𝑏) = 𝑦 ↔ 𝑦 = (𝐴 ⊕ 𝑏)) |
| 13 | 12 | rexbii 3094 |
. . . . . 6
⊢
(∃𝑏 ∈
𝐵 (𝐴 ⊕ 𝑏) = 𝑦 ↔ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏)) |
| 14 | 11, 13 | sylib 218 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) → ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏)) |
| 15 | 14 | ex 412 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) → ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏))) |
| 16 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = (𝐴 ⊕ 𝑏)) → 𝑦 = (𝐴 ⊕ 𝑏)) |
| 17 | | oadif1lem.ord |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑏 ∈ 𝐵 → (𝐴 ⊕ 𝑏) ∈ (𝐴 ⊕ 𝐵))) |
| 18 | 17 | imp 406 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) → (𝐴 ⊕ 𝑏) ∈ (𝐴 ⊕ 𝐵)) |
| 19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = (𝐴 ⊕ 𝑏)) → (𝐴 ⊕ 𝑏) ∈ (𝐴 ⊕ 𝐵)) |
| 20 | 16, 19 | eqeltrd 2841 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = (𝐴 ⊕ 𝑏)) → 𝑦 ∈ (𝐴 ⊕ 𝐵)) |
| 21 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On) |
| 22 | | onelon 6409 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On) |
| 23 | 21, 22 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ On) |
| 24 | | oadif1lem.word |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On) → 𝐴 ⊆ (𝐴 ⊕ 𝑏)) |
| 25 | 1, 23, 24 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ (𝐴 ⊕ 𝑏)) |
| 26 | | oadif1lem.cl2 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On) → (𝐴 ⊕ 𝑏) ∈ On) |
| 27 | 1, 23, 26 | syl2an2r 685 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) → (𝐴 ⊕ 𝑏) ∈ On) |
| 28 | | ontri1 6418 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (𝐴 ⊕ 𝑏) ∈ On) → (𝐴 ⊆ (𝐴 ⊕ 𝑏) ↔ ¬ (𝐴 ⊕ 𝑏) ∈ 𝐴)) |
| 29 | 1, 27, 28 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) → (𝐴 ⊆ (𝐴 ⊕ 𝑏) ↔ ¬ (𝐴 ⊕ 𝑏) ∈ 𝐴)) |
| 30 | 25, 29 | mpbid 232 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) → ¬ (𝐴 ⊕ 𝑏) ∈ 𝐴) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = (𝐴 ⊕ 𝑏)) → ¬ (𝐴 ⊕ 𝑏) ∈ 𝐴) |
| 32 | 16, 31 | eqneltrd 2861 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = (𝐴 ⊕ 𝑏)) → ¬ 𝑦 ∈ 𝐴) |
| 33 | 20, 32 | jca 511 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑏 ∈ 𝐵) ∧ 𝑦 = (𝐴 ⊕ 𝑏)) → (𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
| 34 | 33 | rexlimdva2 3157 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏) → (𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))) |
| 35 | 15, 34 | impbid 212 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) ↔ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏))) |
| 36 | | eldif 3961 |
. . 3
⊢ (𝑦 ∈ ((𝐴 ⊕ 𝐵) ∖ 𝐴) ↔ (𝑦 ∈ (𝐴 ⊕ 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
| 37 | | vex 3484 |
. . . 4
⊢ 𝑦 ∈ V |
| 38 | | eqeq1 2741 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = (𝐴 ⊕ 𝑏) ↔ 𝑦 = (𝐴 ⊕ 𝑏))) |
| 39 | 38 | rexbidv 3179 |
. . . 4
⊢ (𝑥 = 𝑦 → (∃𝑏 ∈ 𝐵 𝑥 = (𝐴 ⊕ 𝑏) ↔ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏))) |
| 40 | 37, 39 | elab 3679 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 ⊕ 𝑏)} ↔ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 ⊕ 𝑏)) |
| 41 | 35, 36, 40 | 3bitr4g 314 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ ((𝐴 ⊕ 𝐵) ∖ 𝐴) ↔ 𝑦 ∈ {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 ⊕ 𝑏)})) |
| 42 | 41 | eqrdv 2735 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ⊕ 𝐵) ∖ 𝐴) = {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 ⊕ 𝑏)}) |