Proof of Theorem ordtuni
Step | Hyp | Ref
| Expression |
1 | | ordtval.1 |
. . . . . 6
⊢ 𝑋 = dom 𝑅 |
2 | | dmexg 6989 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) |
3 | 1, 2 | syl5eqel 2692 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑋 ∈ V) |
4 | | unisng 4388 |
. . . . 5
⊢ (𝑋 ∈ V → ∪ {𝑋}
= 𝑋) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → ∪ {𝑋} = 𝑋) |
6 | 5 | uneq1d 3728 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (∪ {𝑋} ∪ ∪ (𝐴
∪ 𝐵)) = (𝑋 ∪ ∪ (𝐴
∪ 𝐵))) |
7 | | ordtval.2 |
. . . . . . 7
⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) |
8 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋 |
9 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V) |
10 | | elpw2g 4754 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋)) |
12 | 8, 11 | mpbiri 247 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) |
14 | 12, 13 | fmptd 6292 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋) |
15 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋 → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋) |
17 | 7, 16 | syl5eqss 3612 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → 𝐴 ⊆ 𝒫 𝑋) |
18 | | ordtval.3 |
. . . . . . 7
⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) |
19 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ⊆ 𝑋 |
20 | | elpw2g 4754 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ⊆ 𝑋)) |
21 | 9, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ⊆ 𝑋)) |
22 | 19, 21 | mpbiri 247 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ 𝒫 𝑋) |
23 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) |
24 | 22, 23 | fmptd 6292 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}):𝑋⟶𝒫 𝑋) |
25 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}):𝑋⟶𝒫 𝑋 → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⊆ 𝒫 𝑋) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⊆ 𝒫 𝑋) |
27 | 18, 26 | syl5eqss 3612 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → 𝐵 ⊆ 𝒫 𝑋) |
28 | 17, 27 | unssd 3751 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → (𝐴 ∪ 𝐵) ⊆ 𝒫 𝑋) |
29 | | sspwuni 4547 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) ⊆ 𝒫 𝑋 ↔ ∪ (𝐴 ∪ 𝐵) ⊆ 𝑋) |
30 | 28, 29 | sylib 207 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 ∪ 𝐵) ⊆ 𝑋) |
31 | | ssequn2 3748 |
. . . 4
⊢ (∪ (𝐴
∪ 𝐵) ⊆ 𝑋 ↔ (𝑋 ∪ ∪ (𝐴 ∪ 𝐵)) = 𝑋) |
32 | 30, 31 | sylib 207 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (𝑋 ∪ ∪ (𝐴 ∪ 𝐵)) = 𝑋) |
33 | 6, 32 | eqtr2d 2645 |
. 2
⊢ (𝑅 ∈ 𝑉 → 𝑋 = (∪ {𝑋} ∪ ∪ (𝐴
∪ 𝐵))) |
34 | | uniun 4392 |
. 2
⊢ ∪ ({𝑋}
∪ (𝐴 ∪ 𝐵)) = (∪ {𝑋}
∪ ∪ (𝐴 ∪ 𝐵)) |
35 | 33, 34 | syl6eqr 2662 |
1
⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵))) |