Proof of Theorem ordtuni
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ordtval.1 | . . . . . 6
⊢ 𝑋 = dom 𝑅 | 
| 2 |  | dmexg 7924 | . . . . . 6
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V) | 
| 3 | 1, 2 | eqeltrid 2844 | . . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑋 ∈ V) | 
| 4 |  | unisng 4924 | . . . . 5
⊢ (𝑋 ∈ V → ∪ {𝑋}
= 𝑋) | 
| 5 | 3, 4 | syl 17 | . . . 4
⊢ (𝑅 ∈ 𝑉 → ∪ {𝑋} = 𝑋) | 
| 6 | 5 | uneq1d 4166 | . . 3
⊢ (𝑅 ∈ 𝑉 → (∪ {𝑋} ∪ ∪ (𝐴
∪ 𝐵)) = (𝑋 ∪ ∪ (𝐴
∪ 𝐵))) | 
| 7 |  | ordtval.2 | . . . . . . 7
⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) | 
| 8 |  | ssrab2 4079 | . . . . . . . . . 10
⊢ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋 | 
| 9 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ V) | 
| 10 |  | elpw2g 5332 | . . . . . . . . . . 11
⊢ (𝑋 ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋)) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ⊆ 𝑋)) | 
| 12 | 8, 11 | mpbiri 258 | . . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ∈ 𝒫 𝑋) | 
| 13 | 12 | fmpttd 7134 | . . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}):𝑋⟶𝒫 𝑋) | 
| 14 | 13 | frnd 6743 | . . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⊆ 𝒫 𝑋) | 
| 15 | 7, 14 | eqsstrid 4021 | . . . . . 6
⊢ (𝑅 ∈ 𝑉 → 𝐴 ⊆ 𝒫 𝑋) | 
| 16 |  | ordtval.3 | . . . . . . 7
⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) | 
| 17 |  | ssrab2 4079 | . . . . . . . . . 10
⊢ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ⊆ 𝑋 | 
| 18 |  | elpw2g 5332 | . . . . . . . . . . 11
⊢ (𝑋 ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ⊆ 𝑋)) | 
| 19 | 9, 18 | syl 17 | . . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ⊆ 𝑋)) | 
| 20 | 17, 19 | mpbiri 258 | . . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ∈ 𝒫 𝑋) | 
| 21 | 20 | fmpttd 7134 | . . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}):𝑋⟶𝒫 𝑋) | 
| 22 | 21 | frnd 6743 | . . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⊆ 𝒫 𝑋) | 
| 23 | 16, 22 | eqsstrid 4021 | . . . . . 6
⊢ (𝑅 ∈ 𝑉 → 𝐵 ⊆ 𝒫 𝑋) | 
| 24 | 15, 23 | unssd 4191 | . . . . 5
⊢ (𝑅 ∈ 𝑉 → (𝐴 ∪ 𝐵) ⊆ 𝒫 𝑋) | 
| 25 |  | sspwuni 5099 | . . . . 5
⊢ ((𝐴 ∪ 𝐵) ⊆ 𝒫 𝑋 ↔ ∪ (𝐴 ∪ 𝐵) ⊆ 𝑋) | 
| 26 | 24, 25 | sylib 218 | . . . 4
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 ∪ 𝐵) ⊆ 𝑋) | 
| 27 |  | ssequn2 4188 | . . . 4
⊢ (∪ (𝐴
∪ 𝐵) ⊆ 𝑋 ↔ (𝑋 ∪ ∪ (𝐴 ∪ 𝐵)) = 𝑋) | 
| 28 | 26, 27 | sylib 218 | . . 3
⊢ (𝑅 ∈ 𝑉 → (𝑋 ∪ ∪ (𝐴 ∪ 𝐵)) = 𝑋) | 
| 29 | 6, 28 | eqtr2d 2777 | . 2
⊢ (𝑅 ∈ 𝑉 → 𝑋 = (∪ {𝑋} ∪ ∪ (𝐴
∪ 𝐵))) | 
| 30 |  | uniun 4929 | . 2
⊢ ∪ ({𝑋}
∪ (𝐴 ∪ 𝐵)) = (∪ {𝑋}
∪ ∪ (𝐴 ∪ 𝐵)) | 
| 31 | 29, 30 | eqtr4di 2794 | 1
⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵))) |