Proof of Theorem konigthlem
| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑀‘𝑖) ∈ V |
| 2 | | fvex 6919 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑎)‘𝑖) ∈ V |
| 3 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) |
| 4 | 2, 3 | fnmpti 6711 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖) |
| 5 | 1 | mptex 7243 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V |
| 6 | | konigth.4 |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
| 7 | 6 | fvmpt2 7027 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V) → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
| 8 | 5, 7 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
| 9 | 8 | fneq1d 6661 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖) Fn (𝑀‘𝑖) ↔ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖))) |
| 10 | 4, 9 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) Fn (𝑀‘𝑖)) |
| 11 | | fnrndomg 10576 |
. . . . . . . . 9
⊢ ((𝑀‘𝑖) ∈ V → ((𝐷‘𝑖) Fn (𝑀‘𝑖) → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖))) |
| 12 | 1, 10, 11 | mpsyl 68 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐴 → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖)) |
| 13 | | domsdomtr 9152 |
. . . . . . . 8
⊢ ((ran
(𝐷‘𝑖) ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖)) |
| 14 | 12, 13 | sylan 580 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖)) |
| 15 | | sdomdif 9165 |
. . . . . . 7
⊢ (ran
(𝐷‘𝑖) ≺ (𝑁‘𝑖) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅) |
| 16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅) |
| 17 | 16 | ralimiaa 3082 |
. . . . 5
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅) |
| 18 | | konigth.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 19 | | fvex 6919 |
. . . . . . 7
⊢ (𝑁‘𝑖) ∈ V |
| 20 | 19 | difexi 5330 |
. . . . . 6
⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∈ V |
| 21 | 18, 20 | ac6c5 10522 |
. . . . 5
⊢
(∀𝑖 ∈
𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅ → ∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))) |
| 22 | | equid 2011 |
. . . . . . 7
⊢ 𝑓 = 𝑓 |
| 23 | | eldifi 4131 |
. . . . . . . . . . . . 13
⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑒‘𝑖) ∈ (𝑁‘𝑖)) |
| 24 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝑒‘𝑖) ∈ V |
| 25 | | konigth.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) |
| 26 | 25 | fvmpt2 7027 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑒‘𝑖) ∈ V) → (𝐸‘𝑖) = (𝑒‘𝑖)) |
| 27 | 24, 26 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ 𝐴 → (𝐸‘𝑖) = (𝑒‘𝑖)) |
| 28 | 27 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝐴 → ((𝐸‘𝑖) ∈ (𝑁‘𝑖) ↔ (𝑒‘𝑖) ∈ (𝑁‘𝑖))) |
| 29 | 23, 28 | imbitrrid 246 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝐴 → ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸‘𝑖) ∈ (𝑁‘𝑖))) |
| 30 | 29 | ralimia 3080 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)) |
| 31 | 24, 25 | fnmpti 6711 |
. . . . . . . . . . 11
⊢ 𝐸 Fn 𝐴 |
| 32 | 30, 31 | jctil 519 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))) |
| 33 | 18 | mptex 7243 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) ∈ V |
| 34 | 25, 33 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝐸 ∈ V |
| 35 | 34 | elixp 8944 |
. . . . . . . . . 10
⊢ (𝐸 ∈ X𝑖 ∈
𝐴 (𝑁‘𝑖) ↔ (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))) |
| 36 | 32, 35 | sylibr 234 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖)) |
| 37 | | konigth.3 |
. . . . . . . . 9
⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖) |
| 38 | 36, 37 | eleqtrrdi 2852 |
. . . . . . . 8
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ 𝑃) |
| 39 | | foelrn 7127 |
. . . . . . . . . 10
⊢ ((𝑓:𝑆–onto→𝑃 ∧ 𝐸 ∈ 𝑃) → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎)) |
| 40 | 39 | expcom 413 |
. . . . . . . . 9
⊢ (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎))) |
| 41 | | konigth.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) |
| 42 | 41 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪
𝑖 ∈ 𝐴 (𝑀‘𝑖)) |
| 43 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖)) |
| 44 | 42, 43 | bitri 275 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑆 ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖)) |
| 45 | | nfra1 3284 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) |
| 46 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖 𝐸 = (𝑓‘𝑎) |
| 47 | 45, 46 | nfan 1899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖(∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) |
| 48 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖 ¬ 𝑓 = 𝑓 |
| 49 | 27 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = (𝑒‘𝑖)) |
| 50 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸 = (𝑓‘𝑎) → (𝐸‘𝑖) = ((𝑓‘𝑎)‘𝑖)) |
| 51 | 8 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖)‘𝑎) = ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎)) |
| 52 | 3 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ (𝑀‘𝑖) ∧ ((𝑓‘𝑎)‘𝑖) ∈ V) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖)) |
| 53 | 2, 52 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ (𝑀‘𝑖) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖)) |
| 54 | 51, 53 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) = ((𝑓‘𝑎)‘𝑖)) |
| 55 | 54 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝑓‘𝑎)‘𝑖) = ((𝐷‘𝑖)‘𝑎)) |
| 56 | 50, 55 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = ((𝐷‘𝑖)‘𝑎)) |
| 57 | 49, 56 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) = ((𝐷‘𝑖)‘𝑎)) |
| 58 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐷‘𝑖) Fn (𝑀‘𝑖) ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖)) |
| 59 | 10, 58 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖)) |
| 60 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖)) |
| 61 | 57, 60 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
| 62 | 61 | 3adant1 1131 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
| 63 | | simp1 1137 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))) |
| 64 | | simp3l 1202 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → 𝑖 ∈ 𝐴) |
| 65 | | rsp 3247 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))) |
| 66 | | eldifn 4132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
| 67 | 65, 66 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))) |
| 68 | 63, 64, 67 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
| 69 | 62, 68 | pm2.21dd 195 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ 𝑓 = 𝑓) |
| 70 | 69 | 3expia 1122 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ¬ 𝑓 = 𝑓)) |
| 71 | 70 | expd 415 |
. . . . . . . . . . . . . 14
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑖 ∈ 𝐴 → (𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓))) |
| 72 | 47, 48, 71 | rexlimd 3266 |
. . . . . . . . . . . . 13
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓)) |
| 73 | 44, 72 | biimtrid 242 |
. . . . . . . . . . . 12
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓)) |
| 74 | 73 | ex 412 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 = (𝑓‘𝑎) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓))) |
| 75 | 74 | com23 86 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑎 ∈ 𝑆 → (𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓))) |
| 76 | 75 | rexlimdv 3153 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓)) |
| 77 | 40, 76 | syl9r 78 |
. . . . . . . 8
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓))) |
| 78 | 38, 77 | mpd 15 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓)) |
| 79 | 22, 78 | mt2i 137 |
. . . . . 6
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃) |
| 80 | 79 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃) |
| 81 | 17, 21, 80 | 3syl 18 |
. . . 4
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ 𝑓:𝑆–onto→𝑃) |
| 82 | 81 | nexdv 1936 |
. . 3
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ∃𝑓 𝑓:𝑆–onto→𝑃) |
| 83 | 1 | 0dom 9146 |
. . . . . . . 8
⊢ ∅
≼ (𝑀‘𝑖) |
| 84 | | domsdomtr 9152 |
. . . . . . . 8
⊢ ((∅
≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ∅ ≺ (𝑁‘𝑖)) |
| 85 | 83, 84 | mpan 690 |
. . . . . . 7
⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ (𝑁‘𝑖)) |
| 86 | 19 | 0sdom 9147 |
. . . . . . 7
⊢ (∅
≺ (𝑁‘𝑖) ↔ (𝑁‘𝑖) ≠ ∅) |
| 87 | 85, 86 | sylib 218 |
. . . . . 6
⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → (𝑁‘𝑖) ≠ ∅) |
| 88 | 87 | ralimi 3083 |
. . . . 5
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅) |
| 89 | 37 | neeq1i 3005 |
. . . . . 6
⊢ (𝑃 ≠ ∅ ↔ X𝑖 ∈
𝐴 (𝑁‘𝑖) ≠ ∅) |
| 90 | 19 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V |
| 91 | | ixpexg 8962 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V → X𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V) |
| 92 | 90, 91 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V |
| 93 | 37, 92 | eqeltri 2837 |
. . . . . . 7
⊢ 𝑃 ∈ V |
| 94 | 93 | 0sdom 9147 |
. . . . . 6
⊢ (∅
≺ 𝑃 ↔ 𝑃 ≠ ∅) |
| 95 | 18, 19 | ac9 10523 |
. . . . . 6
⊢
(∀𝑖 ∈
𝐴 (𝑁‘𝑖) ≠ ∅ ↔ X𝑖 ∈
𝐴 (𝑁‘𝑖) ≠ ∅) |
| 96 | 89, 94, 95 | 3bitr4i 303 |
. . . . 5
⊢ (∅
≺ 𝑃 ↔
∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅) |
| 97 | 88, 96 | sylibr 234 |
. . . 4
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ 𝑃) |
| 98 | 18, 1 | iunex 7993 |
. . . . . . 7
⊢ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ∈ V |
| 99 | 41, 98 | eqeltri 2837 |
. . . . . 6
⊢ 𝑆 ∈ V |
| 100 | | domtri 10596 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 𝑆 ∈ V) → (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃)) |
| 101 | 93, 99, 100 | mp2an 692 |
. . . . 5
⊢ (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃) |
| 102 | 101 | biimpri 228 |
. . . 4
⊢ (¬
𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆) |
| 103 | | fodomr 9168 |
. . . 4
⊢ ((∅
≺ 𝑃 ∧ 𝑃 ≼ 𝑆) → ∃𝑓 𝑓:𝑆–onto→𝑃) |
| 104 | 97, 102, 103 | syl2an 596 |
. . 3
⊢
((∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) ∧ ¬ 𝑆 ≺ 𝑃) → ∃𝑓 𝑓:𝑆–onto→𝑃) |
| 105 | 82, 104 | mtand 816 |
. 2
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ¬ 𝑆 ≺ 𝑃) |
| 106 | 105 | notnotrd 133 |
1
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃) |