Step | Hyp | Ref
| Expression |
1 | | fodjuf.fo |
. . . . 5
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) |
2 | | djulcl 7028 |
. . . . 5
⊢ (𝑢 ∈ 𝐴 → (inl‘𝑢) ∈ (𝐴 ⊔ 𝐵)) |
3 | | foelrn 5732 |
. . . . 5
⊢ ((𝐹:𝑂–onto→(𝐴 ⊔ 𝐵) ∧ (inl‘𝑢) ∈ (𝐴 ⊔ 𝐵)) → ∃𝑣 ∈ 𝑂 (inl‘𝑢) = (𝐹‘𝑣)) |
4 | 1, 2, 3 | syl2an 287 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ∃𝑣 ∈ 𝑂 (inl‘𝑢) = (𝐹‘𝑣)) |
5 | | fodjuf.p |
. . . . . 6
⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o)) |
6 | | fveqeq2 5505 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ((𝐹‘𝑦) = (inl‘𝑧) ↔ (𝐹‘𝑣) = (inl‘𝑧))) |
7 | 6 | rexbidv 2471 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → (∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧) ↔ ∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧))) |
8 | 7 | ifbid 3547 |
. . . . . 6
⊢ (𝑦 = 𝑣 → if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o) = if(∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧), ∅, 1o)) |
9 | | simprl 526 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → 𝑣 ∈ 𝑂) |
10 | | peano1 4578 |
. . . . . . . 8
⊢ ∅
∈ ω |
11 | 10 | a1i 9 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → ∅ ∈
ω) |
12 | | 1onn 6499 |
. . . . . . . 8
⊢
1o ∈ ω |
13 | 12 | a1i 9 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → 1o ∈
ω) |
14 | 1 | fodjuomnilemdc 7120 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧)) |
15 | 14 | ad2ant2r 506 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧)) |
16 | 11, 13, 15 | ifcldcd 3561 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → if(∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧), ∅, 1o) ∈
ω) |
17 | 5, 8, 9, 16 | fvmptd3 5589 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → (𝑃‘𝑣) = if(∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧), ∅, 1o)) |
18 | | fveqeq2 5505 |
. . . . . 6
⊢ (𝑤 = 𝑣 → ((𝑃‘𝑤) = 1o ↔ (𝑃‘𝑣) = 1o)) |
19 | | fodju0.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ 𝑂 (𝑃‘𝑤) = 1o) |
20 | 19 | ad2antrr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → ∀𝑤 ∈ 𝑂 (𝑃‘𝑤) = 1o) |
21 | 18, 20, 9 | rspcdva 2839 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → (𝑃‘𝑣) = 1o) |
22 | | simplr 525 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → 𝑢 ∈ 𝐴) |
23 | | simprr 527 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → (inl‘𝑢) = (𝐹‘𝑣)) |
24 | 23 | eqcomd 2176 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → (𝐹‘𝑣) = (inl‘𝑢)) |
25 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → (inl‘𝑧) = (inl‘𝑢)) |
26 | 25 | rspceeqv 2852 |
. . . . . . 7
⊢ ((𝑢 ∈ 𝐴 ∧ (𝐹‘𝑣) = (inl‘𝑢)) → ∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧)) |
27 | 22, 24, 26 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → ∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧)) |
28 | 27 | iftrued 3533 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → if(∃𝑧 ∈ 𝐴 (𝐹‘𝑣) = (inl‘𝑧), ∅, 1o) =
∅) |
29 | 17, 21, 28 | 3eqtr3rd 2212 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ (𝑣 ∈ 𝑂 ∧ (inl‘𝑢) = (𝐹‘𝑣))) → ∅ =
1o) |
30 | 4, 29 | rexlimddv 2592 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ∅ =
1o) |
31 | | 1n0 6411 |
. . . . 5
⊢
1o ≠ ∅ |
32 | 31 | nesymi 2386 |
. . . 4
⊢ ¬
∅ = 1o |
33 | 32 | a1i 9 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ¬ ∅ =
1o) |
34 | 30, 33 | pm2.65da 656 |
. 2
⊢ (𝜑 → ¬ 𝑢 ∈ 𝐴) |
35 | 34 | eq0rdv 3459 |
1
⊢ (𝜑 → 𝐴 = ∅) |