Step | Hyp | Ref
| Expression |
1 | | joindef.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ 𝑉) |
2 | | joindef.u |
. . . . . . 7
⊢ 𝑈 = (lub‘𝐾) |
3 | | joindef.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
4 | 2, 3 | joinfval2 16825 |
. . . . . 6
⊢ (𝐾 ∈ 𝑉 → ∨ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → ∨ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}) |
6 | 5 | oveqd 6566 |
. . . 4
⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑋{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}𝑌)) |
7 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑋 ∨ 𝑌) = (𝑋{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}𝑌)) |
8 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ {𝑋, 𝑌} ∈ dom 𝑈) → {𝑋, 𝑌} ∈ dom 𝑈) |
9 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑈‘{𝑋, 𝑌}) = (𝑈‘{𝑋, 𝑌})) |
10 | | joindef.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
11 | | joindef.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑍) |
12 | | fvex 6113 |
. . . . . . 7
⊢ (𝑈‘{𝑋, 𝑌}) ∈ V |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑈‘{𝑋, 𝑌}) ∈ V) |
14 | | preq12 4214 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → {𝑥, 𝑦} = {𝑋, 𝑌}) |
15 | 14 | eleq1d 2672 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ({𝑥, 𝑦} ∈ dom 𝑈 ↔ {𝑋, 𝑌} ∈ dom 𝑈)) |
16 | 15 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑈‘{𝑋, 𝑌})) → ({𝑥, 𝑦} ∈ dom 𝑈 ↔ {𝑋, 𝑌} ∈ dom 𝑈)) |
17 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑈‘{𝑋, 𝑌})) → 𝑧 = (𝑈‘{𝑋, 𝑌})) |
18 | 14 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝑈‘{𝑥, 𝑦}) = (𝑈‘{𝑋, 𝑌})) |
19 | 18 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑈‘{𝑋, 𝑌})) → (𝑈‘{𝑥, 𝑦}) = (𝑈‘{𝑋, 𝑌})) |
20 | 17, 19 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑈‘{𝑋, 𝑌})) → (𝑧 = (𝑈‘{𝑥, 𝑦}) ↔ (𝑈‘{𝑋, 𝑌}) = (𝑈‘{𝑋, 𝑌}))) |
21 | 16, 20 | anbi12d 743 |
. . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑈‘{𝑋, 𝑌})) → (({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦})) ↔ ({𝑋, 𝑌} ∈ dom 𝑈 ∧ (𝑈‘{𝑋, 𝑌}) = (𝑈‘{𝑋, 𝑌})))) |
22 | | moeq 3349 |
. . . . . . . 8
⊢
∃*𝑧 𝑧 = (𝑈‘{𝑥, 𝑦}) |
23 | 22 | moani 2513 |
. . . . . . 7
⊢
∃*𝑧({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦})) |
24 | | eqid 2610 |
. . . . . . 7
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))} |
25 | 21, 23, 24 | ovigg 6679 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑍 ∧ (𝑈‘{𝑋, 𝑌}) ∈ V) → (({𝑋, 𝑌} ∈ dom 𝑈 ∧ (𝑈‘{𝑋, 𝑌}) = (𝑈‘{𝑋, 𝑌})) → (𝑋{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}𝑌) = (𝑈‘{𝑋, 𝑌}))) |
26 | 10, 11, 13, 25 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (({𝑋, 𝑌} ∈ dom 𝑈 ∧ (𝑈‘{𝑋, 𝑌}) = (𝑈‘{𝑋, 𝑌})) → (𝑋{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}𝑌) = (𝑈‘{𝑋, 𝑌}))) |
27 | 26 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ {𝑋, 𝑌} ∈ dom 𝑈) → (({𝑋, 𝑌} ∈ dom 𝑈 ∧ (𝑈‘{𝑋, 𝑌}) = (𝑈‘{𝑋, 𝑌})) → (𝑋{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}𝑌) = (𝑈‘{𝑋, 𝑌}))) |
28 | 8, 9, 27 | mp2and 711 |
. . 3
⊢ ((𝜑 ∧ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑋{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))}𝑌) = (𝑈‘{𝑋, 𝑌})) |
29 | 7, 28 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑋 ∨ 𝑌) = (𝑈‘{𝑋, 𝑌})) |
30 | 2, 3, 1, 10, 11 | joindef 16827 |
. . . . . 6
⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈)) |
31 | 30 | notbid 307 |
. . . . 5
⊢ (𝜑 → (¬ 〈𝑋, 𝑌〉 ∈ dom ∨ ↔ ¬ {𝑋, 𝑌} ∈ dom 𝑈)) |
32 | | df-ov 6552 |
. . . . . 6
⊢ (𝑋 ∨ 𝑌) = ( ∨ ‘〈𝑋, 𝑌〉) |
33 | | ndmfv 6128 |
. . . . . 6
⊢ (¬
〈𝑋, 𝑌〉 ∈ dom ∨ → ( ∨
‘〈𝑋, 𝑌〉) =
∅) |
34 | 32, 33 | syl5eq 2656 |
. . . . 5
⊢ (¬
〈𝑋, 𝑌〉 ∈ dom ∨ → (𝑋 ∨ 𝑌) = ∅) |
35 | 31, 34 | syl6bir 243 |
. . . 4
⊢ (𝜑 → (¬ {𝑋, 𝑌} ∈ dom 𝑈 → (𝑋 ∨ 𝑌) = ∅)) |
36 | 35 | imp 444 |
. . 3
⊢ ((𝜑 ∧ ¬ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑋 ∨ 𝑌) = ∅) |
37 | | ndmfv 6128 |
. . . 4
⊢ (¬
{𝑋, 𝑌} ∈ dom 𝑈 → (𝑈‘{𝑋, 𝑌}) = ∅) |
38 | 37 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑈‘{𝑋, 𝑌}) = ∅) |
39 | 36, 38 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ ¬ {𝑋, 𝑌} ∈ dom 𝑈) → (𝑋 ∨ 𝑌) = (𝑈‘{𝑋, 𝑌})) |
40 | 29, 39 | pm2.61dan 828 |
1
⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑈‘{𝑋, 𝑌})) |