Step | Hyp | Ref
| Expression |
1 | | fodjuomnilemdc.fo |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) |
2 | | fof 5392 |
. . . . . 6
⊢ (𝐹:𝑂–onto→(𝐴 ⊔ 𝐵) → 𝐹:𝑂⟶(𝐴 ⊔ 𝐵)) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑂⟶(𝐴 ⊔ 𝐵)) |
4 | 3 | ffvelrnda 5602 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → (𝐹‘𝑋) ∈ (𝐴 ⊔ 𝐵)) |
5 | | djur 7013 |
. . . 4
⊢ ((𝐹‘𝑋) ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ∨ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧))) |
6 | 4, 5 | sylib 121 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → (∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ∨ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧))) |
7 | | nfv 1508 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝜑 ∧ 𝑋 ∈ 𝑂) |
8 | | nfre1 2500 |
. . . . . . . 8
⊢
Ⅎ𝑧∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧) |
9 | 7, 8 | nfan 1545 |
. . . . . . 7
⊢
Ⅎ𝑧((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) |
10 | | simpr 109 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) |
11 | | fveq2 5468 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (inr‘𝑧) = (inr‘𝑤)) |
12 | 11 | eqeq2d 2169 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝐹‘𝑋) = (inr‘𝑧) ↔ (𝐹‘𝑋) = (inr‘𝑤))) |
13 | 12 | cbvrexv 2681 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝐵 (𝐹‘𝑋) = (inr‘𝑧) ↔ ∃𝑤 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑤)) |
14 | 10, 13 | sylib 121 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → ∃𝑤 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑤)) |
15 | | vex 2715 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
16 | | vex 2715 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
17 | | djune 7022 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) →
(inl‘𝑧) ≠
(inr‘𝑤)) |
18 | 15, 16, 17 | mp2an 423 |
. . . . . . . . . . . . . 14
⊢
(inl‘𝑧) ≠
(inr‘𝑤) |
19 | | neeq2 2341 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑋) = (inr‘𝑤) → ((inl‘𝑧) ≠ (𝐹‘𝑋) ↔ (inl‘𝑧) ≠ (inr‘𝑤))) |
20 | 18, 19 | mpbiri 167 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑋) = (inr‘𝑤) → (inl‘𝑧) ≠ (𝐹‘𝑋)) |
21 | 20 | necomd 2413 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑋) = (inr‘𝑤) → (𝐹‘𝑋) ≠ (inl‘𝑧)) |
22 | 21 | neneqd 2348 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑋) = (inr‘𝑤) → ¬ (𝐹‘𝑋) = (inl‘𝑧)) |
23 | 22 | a1i 9 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → ((𝐹‘𝑋) = (inr‘𝑤) → ¬ (𝐹‘𝑋) = (inl‘𝑧))) |
24 | 23 | rexlimdvw 2578 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → (∃𝑤 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑤) → ¬ (𝐹‘𝑋) = (inl‘𝑧))) |
25 | 14, 24 | mpd 13 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → ¬ (𝐹‘𝑋) = (inl‘𝑧)) |
26 | 25 | a1d 22 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → (𝑧 ∈ 𝐴 → ¬ (𝐹‘𝑋) = (inl‘𝑧))) |
27 | 9, 26 | ralrimi 2528 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → ∀𝑧 ∈ 𝐴 ¬ (𝐹‘𝑋) = (inl‘𝑧)) |
28 | | ralnex 2445 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 ¬ (𝐹‘𝑋) = (inl‘𝑧) ↔ ¬ ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) |
29 | 27, 28 | sylib 121 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ 𝑂) ∧ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → ¬ ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) |
30 | 29 | ex 114 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → (∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧) → ¬ ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧))) |
31 | 30 | orim2d 778 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → ((∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ∨ ∃𝑧 ∈ 𝐵 (𝐹‘𝑋) = (inr‘𝑧)) → (∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ∨ ¬ ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)))) |
32 | 6, 31 | mpd 13 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → (∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ∨ ¬ ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧))) |
33 | | df-dc 821 |
. 2
⊢
(DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ↔ (∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧) ∨ ¬ ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧))) |
34 | 32, 33 | sylibr 133 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) |