| Step | Hyp | Ref
| Expression |
| 1 | | snex 5436 |
. . . . . 6
⊢ {𝑋} ∈ V |
| 2 | | ssun2 4179 |
. . . . . . 7
⊢ (𝐴 ∪ 𝐵) ⊆ ({𝑋} ∪ (𝐴 ∪ 𝐵)) |
| 3 | | ordtval.1 |
. . . . . . . . . 10
⊢ 𝑋 = dom 𝑅 |
| 4 | | ordtval.2 |
. . . . . . . . . 10
⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) |
| 5 | | ordtval.3 |
. . . . . . . . . 10
⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) |
| 6 | 3, 4, 5 | ordtuni 23198 |
. . . . . . . . 9
⊢ (𝑅 ∈ TosetRel → 𝑋 = ∪
({𝑋} ∪ (𝐴 ∪ 𝐵))) |
| 7 | | dmexg 7923 |
. . . . . . . . . 10
⊢ (𝑅 ∈ TosetRel → dom
𝑅 ∈
V) |
| 8 | 3, 7 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝑅 ∈ TosetRel → 𝑋 ∈ V) |
| 9 | 6, 8 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝑅 ∈ TosetRel → ∪ ({𝑋}
∪ (𝐴 ∪ 𝐵)) ∈ V) |
| 10 | | uniexb 7784 |
. . . . . . . 8
⊢ (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V ↔ ∪ ({𝑋}
∪ (𝐴 ∪ 𝐵)) ∈ V) |
| 11 | 9, 10 | sylibr 234 |
. . . . . . 7
⊢ (𝑅 ∈ TosetRel → ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V) |
| 12 | | ssexg 5323 |
. . . . . . 7
⊢ (((𝐴 ∪ 𝐵) ⊆ ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∧ ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
| 13 | 2, 11, 12 | sylancr 587 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝐴 ∪ 𝐵) ∈ V) |
| 14 | | elfiun 9470 |
. . . . . 6
⊢ (({𝑋} ∈ V ∧ (𝐴 ∪ 𝐵) ∈ V) → (𝑧 ∈ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) ↔ (𝑧 ∈ (fi‘{𝑋}) ∨ 𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) ∨ ∃𝑚 ∈ (fi‘{𝑋})∃𝑛 ∈ (fi‘(𝐴 ∪ 𝐵))𝑧 = (𝑚 ∩ 𝑛)))) |
| 15 | 1, 13, 14 | sylancr 587 |
. . . . 5
⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) ↔ (𝑧 ∈ (fi‘{𝑋}) ∨ 𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) ∨ ∃𝑚 ∈ (fi‘{𝑋})∃𝑛 ∈ (fi‘(𝐴 ∪ 𝐵))𝑧 = (𝑚 ∩ 𝑛)))) |
| 16 | | fisn 9467 |
. . . . . . . . 9
⊢
(fi‘{𝑋}) =
{𝑋} |
| 17 | | ssun1 4178 |
. . . . . . . . 9
⊢ {𝑋} ⊆ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)) |
| 18 | 16, 17 | eqsstri 4030 |
. . . . . . . 8
⊢
(fi‘{𝑋})
⊆ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)) |
| 19 | 18 | sseli 3979 |
. . . . . . 7
⊢ (𝑧 ∈ (fi‘{𝑋}) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 20 | 19 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘{𝑋}) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 21 | | ordtval.4 |
. . . . . . . . 9
⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) |
| 22 | 3, 4, 5, 21 | ordtbas2 23199 |
. . . . . . . 8
⊢ (𝑅 ∈ TosetRel →
(fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶)) |
| 23 | | ssun2 4179 |
. . . . . . . 8
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) ⊆ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)) |
| 24 | 22, 23 | eqsstrdi 4028 |
. . . . . . 7
⊢ (𝑅 ∈ TosetRel →
(fi‘(𝐴 ∪ 𝐵)) ⊆ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 25 | 24 | sseld 3982 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 26 | | fipwuni 9466 |
. . . . . . . . . . . . . . 15
⊢
(fi‘(𝐴 ∪
𝐵)) ⊆ 𝒫 ∪ (𝐴
∪ 𝐵) |
| 27 | 26 | sseli 3979 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)) → 𝑛 ∈ 𝒫 ∪ (𝐴
∪ 𝐵)) |
| 28 | 27 | elpwid 4609 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)) → 𝑛 ⊆ ∪ (𝐴 ∪ 𝐵)) |
| 29 | 28 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑛 ⊆ ∪ (𝐴 ∪ 𝐵)) |
| 30 | 2 | unissi 4916 |
. . . . . . . . . . . . . 14
⊢ ∪ (𝐴
∪ 𝐵) ⊆ ∪ ({𝑋}
∪ (𝐴 ∪ 𝐵)) |
| 31 | 30, 6 | sseqtrrid 4027 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ TosetRel → ∪ (𝐴
∪ 𝐵) ⊆ 𝑋) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → ∪
(𝐴 ∪ 𝐵) ⊆ 𝑋) |
| 33 | 29, 32 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑛 ⊆ 𝑋) |
| 34 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑚 ∈ (fi‘{𝑋})) |
| 35 | 34, 16 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑚 ∈ {𝑋}) |
| 36 | | elsni 4643 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ {𝑋} → 𝑚 = 𝑋) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑚 = 𝑋) |
| 38 | 33, 37 | sseqtrrd 4021 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑛 ⊆ 𝑚) |
| 39 | | sseqin2 4223 |
. . . . . . . . . 10
⊢ (𝑛 ⊆ 𝑚 ↔ (𝑚 ∩ 𝑛) = 𝑛) |
| 40 | 38, 39 | sylib 218 |
. . . . . . . . 9
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → (𝑚 ∩ 𝑛) = 𝑛) |
| 41 | 24 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ TosetRel ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵))) → 𝑛 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 42 | 41 | adantrl 716 |
. . . . . . . . 9
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → 𝑛 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 43 | 40, 42 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → (𝑚 ∩ 𝑛) ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 44 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑧 = (𝑚 ∩ 𝑛) → (𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)) ↔ (𝑚 ∩ 𝑛) ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 45 | 43, 44 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘{𝑋}) ∧ 𝑛 ∈ (fi‘(𝐴 ∪ 𝐵)))) → (𝑧 = (𝑚 ∩ 𝑛) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 46 | 45 | rexlimdvva 3213 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel →
(∃𝑚 ∈
(fi‘{𝑋})∃𝑛 ∈ (fi‘(𝐴 ∪ 𝐵))𝑧 = (𝑚 ∩ 𝑛) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 47 | 20, 25, 46 | 3jaod 1431 |
. . . . 5
⊢ (𝑅 ∈ TosetRel → ((𝑧 ∈ (fi‘{𝑋}) ∨ 𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) ∨ ∃𝑚 ∈ (fi‘{𝑋})∃𝑛 ∈ (fi‘(𝐴 ∪ 𝐵))𝑧 = (𝑚 ∩ 𝑛)) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 48 | 15, 47 | sylbid 240 |
. . . 4
⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) → 𝑧 ∈ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)))) |
| 49 | 48 | ssrdv 3989 |
. . 3
⊢ (𝑅 ∈ TosetRel →
(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) ⊆ ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 50 | | ssfii 9459 |
. . . . . 6
⊢ (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V → ({𝑋} ∪ (𝐴 ∪ 𝐵)) ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 51 | 11, 50 | syl 17 |
. . . . 5
⊢ (𝑅 ∈ TosetRel → ({𝑋} ∪ (𝐴 ∪ 𝐵)) ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 52 | 51 | unssad 4193 |
. . . 4
⊢ (𝑅 ∈ TosetRel → {𝑋} ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 53 | | fiss 9464 |
. . . . . 6
⊢ ((({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V ∧ (𝐴 ∪ 𝐵) ⊆ ({𝑋} ∪ (𝐴 ∪ 𝐵))) → (fi‘(𝐴 ∪ 𝐵)) ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 54 | 11, 2, 53 | sylancl 586 |
. . . . 5
⊢ (𝑅 ∈ TosetRel →
(fi‘(𝐴 ∪ 𝐵)) ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 55 | 22, 54 | eqsstrrd 4019 |
. . . 4
⊢ (𝑅 ∈ TosetRel → ((𝐴 ∪ 𝐵) ∪ 𝐶) ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 56 | 52, 55 | unssd 4192 |
. . 3
⊢ (𝑅 ∈ TosetRel → ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)) ⊆ (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))) |
| 57 | 49, 56 | eqssd 4001 |
. 2
⊢ (𝑅 ∈ TosetRel →
(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) = ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶))) |
| 58 | | unass 4172 |
. 2
⊢ (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∪ 𝐶) = ({𝑋} ∪ ((𝐴 ∪ 𝐵) ∪ 𝐶)) |
| 59 | 57, 58 | eqtr4di 2795 |
1
⊢ (𝑅 ∈ TosetRel →
(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) = (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∪ 𝐶)) |