Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . 3
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝐴 = ∅) → 𝐴 = ∅) |
2 | | 0ex 4790 |
. . 3
⊢ ∅
∈ V |
3 | 1, 2 | syl6eqel 2709 |
. 2
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝐴 = ∅) → 𝐴 ∈ V) |
4 | | n0 3931 |
. . 3
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
5 | | snex 4908 |
. . . . . . . . 9
⊢ {𝑥} ∈ V |
6 | | dmexg 7097 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
7 | | rnexg 7098 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V) |
8 | | unexg 6959 |
. . . . . . . . . 10
⊢ ((dom
𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
9 | 6, 7, 8 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V) |
10 | | unexg 6959 |
. . . . . . . . 9
⊢ (({𝑥} ∈ V ∧ (dom 𝑅 ∪ ran 𝑅) ∈ V) → ({𝑥} ∪ (dom 𝑅 ∪ ran 𝑅)) ∈ V) |
11 | 5, 9, 10 | sylancr 695 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → ({𝑥} ∪ (dom 𝑅 ∪ ran 𝑅)) ∈ V) |
12 | 11 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝑥 ∈ 𝐴) → ({𝑥} ∪ (dom 𝑅 ∪ ran 𝑅)) ∈ V) |
13 | | sossfld 5580 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
14 | 13 | adantlr 751 |
. . . . . . . 8
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
15 | | ssundif 4052 |
. . . . . . . 8
⊢ (𝐴 ⊆ ({𝑥} ∪ (dom 𝑅 ∪ ran 𝑅)) ↔ (𝐴 ∖ {𝑥}) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
16 | 14, 15 | sylibr 224 |
. . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ ({𝑥} ∪ (dom 𝑅 ∪ ran 𝑅))) |
17 | 12, 16 | ssexd 4805 |
. . . . . 6
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ V) |
18 | 17 | ex 450 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) → (𝑥 ∈ 𝐴 → 𝐴 ∈ V)) |
19 | 18 | exlimdv 1861 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) → (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ∈ V)) |
20 | 19 | imp 445 |
. . 3
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ ∃𝑥 𝑥 ∈ 𝐴) → 𝐴 ∈ V) |
21 | 4, 20 | sylan2b 492 |
. 2
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ V) |
22 | 3, 21 | pm2.61dane 2881 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) → 𝐴 ∈ V) |