Proof of Theorem konigthlem
Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝑀‘𝑖) ∈ V |
2 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑎)‘𝑖) ∈ V |
3 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) |
4 | 2, 3 | fnmpti 5935 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖) |
5 | 1 | mptex 6390 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V |
6 | | konigth.4 |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
7 | 6 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) ∈ V) → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
8 | 5, 7 | mpan2 703 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
9 | 8 | fneq1d 5895 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖) Fn (𝑀‘𝑖) ↔ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) Fn (𝑀‘𝑖))) |
10 | 4, 9 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑖 ∈ 𝐴 → (𝐷‘𝑖) Fn (𝑀‘𝑖)) |
11 | | fnrndomg 9239 |
. . . . . . . . 9
⊢ ((𝑀‘𝑖) ∈ V → ((𝐷‘𝑖) Fn (𝑀‘𝑖) → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖))) |
12 | 1, 10, 11 | mpsyl 66 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐴 → ran (𝐷‘𝑖) ≼ (𝑀‘𝑖)) |
13 | | domsdomtr 7980 |
. . . . . . . 8
⊢ ((ran
(𝐷‘𝑖) ≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖)) |
14 | 12, 13 | sylan 487 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ran (𝐷‘𝑖) ≺ (𝑁‘𝑖)) |
15 | | sdomdif 7993 |
. . . . . . 7
⊢ (ran
(𝐷‘𝑖) ≺ (𝑁‘𝑖) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅) |
17 | 16 | ralimiaa 2935 |
. . . . 5
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅) |
18 | | konigth.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
19 | | fvex 6113 |
. . . . . . 7
⊢ (𝑁‘𝑖) ∈ V |
20 | | difss 3699 |
. . . . . . 7
⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ⊆ (𝑁‘𝑖) |
21 | 19, 20 | ssexi 4731 |
. . . . . 6
⊢ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∈ V |
22 | 18, 21 | ac6c5 9187 |
. . . . 5
⊢
(∀𝑖 ∈
𝐴 ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ≠ ∅ → ∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))) |
23 | | equid 1926 |
. . . . . . 7
⊢ 𝑓 = 𝑓 |
24 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑒‘𝑖) ∈ (𝑁‘𝑖)) |
25 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝑒‘𝑖) ∈ V |
26 | | konigth.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) |
27 | 26 | fvmpt2 6200 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑒‘𝑖) ∈ V) → (𝐸‘𝑖) = (𝑒‘𝑖)) |
28 | 25, 27 | mpan2 703 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ 𝐴 → (𝐸‘𝑖) = (𝑒‘𝑖)) |
29 | 28 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ 𝐴 → ((𝐸‘𝑖) ∈ (𝑁‘𝑖) ↔ (𝑒‘𝑖) ∈ (𝑁‘𝑖))) |
30 | 24, 29 | syl5ibr 235 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝐴 → ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸‘𝑖) ∈ (𝑁‘𝑖))) |
31 | 30 | ralimia 2934 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖)) |
32 | 25, 26 | fnmpti 5935 |
. . . . . . . . . . 11
⊢ 𝐸 Fn 𝐴 |
33 | 31, 32 | jctil 558 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))) |
34 | 18 | mptex 6390 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) ∈ V |
35 | 26, 34 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐸 ∈ V |
36 | 35 | elixp 7801 |
. . . . . . . . . 10
⊢ (𝐸 ∈ X𝑖 ∈
𝐴 (𝑁‘𝑖) ↔ (𝐸 Fn 𝐴 ∧ ∀𝑖 ∈ 𝐴 (𝐸‘𝑖) ∈ (𝑁‘𝑖))) |
37 | 33, 36 | sylibr 223 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ X𝑖 ∈ 𝐴 (𝑁‘𝑖)) |
38 | | konigth.3 |
. . . . . . . . 9
⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖) |
39 | 37, 38 | syl6eleqr 2699 |
. . . . . . . 8
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → 𝐸 ∈ 𝑃) |
40 | | foelrn 6286 |
. . . . . . . . . 10
⊢ ((𝑓:𝑆–onto→𝑃 ∧ 𝐸 ∈ 𝑃) → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎)) |
41 | 40 | expcom 450 |
. . . . . . . . 9
⊢ (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎))) |
42 | | konigth.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) |
43 | 42 | eleq2i 2680 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪
𝑖 ∈ 𝐴 (𝑀‘𝑖)) |
44 | | eliun 4460 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖)) |
45 | 43, 44 | bitri 263 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑆 ↔ ∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖)) |
46 | | nfra1 2925 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) |
47 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖 𝐸 = (𝑓‘𝑎) |
48 | 46, 47 | nfan 1816 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖(∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) |
49 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖 ¬ 𝑓 = 𝑓 |
50 | 28 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = (𝑒‘𝑖)) |
51 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸 = (𝑓‘𝑎) → (𝐸‘𝑖) = ((𝑓‘𝑎)‘𝑖)) |
52 | 8 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝐴 → ((𝐷‘𝑖)‘𝑎) = ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎)) |
53 | 3 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ (𝑀‘𝑖) ∧ ((𝑓‘𝑎)‘𝑖) ∈ V) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖)) |
54 | 2, 53 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ (𝑀‘𝑖) → ((𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))‘𝑎) = ((𝑓‘𝑎)‘𝑖)) |
55 | 52, 54 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) = ((𝑓‘𝑎)‘𝑖)) |
56 | 55 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝑓‘𝑎)‘𝑖) = ((𝐷‘𝑖)‘𝑎)) |
57 | 51, 56 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝐸‘𝑖) = ((𝐷‘𝑖)‘𝑎)) |
58 | 50, 57 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) = ((𝐷‘𝑖)‘𝑎)) |
59 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐷‘𝑖) Fn (𝑀‘𝑖) ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖)) |
60 | 10, 59 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖)) |
61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ((𝐷‘𝑖)‘𝑎) ∈ ran (𝐷‘𝑖)) |
62 | 58, 61 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
63 | 62 | 3adant1 1072 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
64 | | simp1 1054 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖))) |
65 | | simp3l 1082 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → 𝑖 ∈ 𝐴) |
66 | | rsp 2913 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)))) |
67 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
68 | 66, 67 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑖 ∈ 𝐴 → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖))) |
69 | 64, 65, 68 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ (𝑒‘𝑖) ∈ ran (𝐷‘𝑖)) |
70 | 63, 69 | pm2.21dd 185 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎) ∧ (𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖))) → ¬ 𝑓 = 𝑓) |
71 | 70 | 3expia 1259 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → ((𝑖 ∈ 𝐴 ∧ 𝑎 ∈ (𝑀‘𝑖)) → ¬ 𝑓 = 𝑓)) |
72 | 71 | expd 451 |
. . . . . . . . . . . . . 14
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑖 ∈ 𝐴 → (𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓))) |
73 | 48, 49, 72 | rexlimd 3008 |
. . . . . . . . . . . . 13
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (∃𝑖 ∈ 𝐴 𝑎 ∈ (𝑀‘𝑖) → ¬ 𝑓 = 𝑓)) |
74 | 45, 73 | syl5bi 231 |
. . . . . . . . . . . 12
⊢
((∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) ∧ 𝐸 = (𝑓‘𝑎)) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓)) |
75 | 74 | ex 449 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 = (𝑓‘𝑎) → (𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓))) |
76 | 75 | com23 84 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑎 ∈ 𝑆 → (𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓))) |
77 | 76 | rexlimdv 3012 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (∃𝑎 ∈ 𝑆 𝐸 = (𝑓‘𝑎) → ¬ 𝑓 = 𝑓)) |
78 | 41, 77 | syl9r 76 |
. . . . . . . 8
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝐸 ∈ 𝑃 → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓))) |
79 | 39, 78 | mpd 15 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → (𝑓:𝑆–onto→𝑃 → ¬ 𝑓 = 𝑓)) |
80 | 23, 79 | mt2i 131 |
. . . . . 6
⊢
(∀𝑖 ∈
𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃) |
81 | 80 | exlimiv 1845 |
. . . . 5
⊢
(∃𝑒∀𝑖 ∈ 𝐴 (𝑒‘𝑖) ∈ ((𝑁‘𝑖) ∖ ran (𝐷‘𝑖)) → ¬ 𝑓:𝑆–onto→𝑃) |
82 | 17, 22, 81 | 3syl 18 |
. . . 4
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ 𝑓:𝑆–onto→𝑃) |
83 | 82 | nexdv 1851 |
. . 3
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ∃𝑓 𝑓:𝑆–onto→𝑃) |
84 | 1 | 0dom 7975 |
. . . . . . . 8
⊢ ∅
≼ (𝑀‘𝑖) |
85 | | domsdomtr 7980 |
. . . . . . . 8
⊢ ((∅
≼ (𝑀‘𝑖) ∧ (𝑀‘𝑖) ≺ (𝑁‘𝑖)) → ∅ ≺ (𝑁‘𝑖)) |
86 | 84, 85 | mpan 702 |
. . . . . . 7
⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ (𝑁‘𝑖)) |
87 | 19 | 0sdom 7976 |
. . . . . . 7
⊢ (∅
≺ (𝑁‘𝑖) ↔ (𝑁‘𝑖) ≠ ∅) |
88 | 86, 87 | sylib 207 |
. . . . . 6
⊢ ((𝑀‘𝑖) ≺ (𝑁‘𝑖) → (𝑁‘𝑖) ≠ ∅) |
89 | 88 | ralimi 2936 |
. . . . 5
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅) |
90 | 38 | neeq1i 2846 |
. . . . . 6
⊢ (𝑃 ≠ ∅ ↔ X𝑖 ∈
𝐴 (𝑁‘𝑖) ≠ ∅) |
91 | 19 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V |
92 | | ixpexg 7818 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V → X𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V) |
93 | 91, 92 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑖 ∈
𝐴 (𝑁‘𝑖) ∈ V |
94 | 38, 93 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑃 ∈ V |
95 | 94 | 0sdom 7976 |
. . . . . 6
⊢ (∅
≺ 𝑃 ↔ 𝑃 ≠ ∅) |
96 | 18, 19 | ac9 9188 |
. . . . . 6
⊢
(∀𝑖 ∈
𝐴 (𝑁‘𝑖) ≠ ∅ ↔ X𝑖 ∈
𝐴 (𝑁‘𝑖) ≠ ∅) |
97 | 90, 95, 96 | 3bitr4i 291 |
. . . . 5
⊢ (∅
≺ 𝑃 ↔
∀𝑖 ∈ 𝐴 (𝑁‘𝑖) ≠ ∅) |
98 | 89, 97 | sylibr 223 |
. . . 4
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ∅ ≺ 𝑃) |
99 | 18, 1 | iunex 7039 |
. . . . . . 7
⊢ ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) ∈ V |
100 | 42, 99 | eqeltri 2684 |
. . . . . 6
⊢ 𝑆 ∈ V |
101 | | domtri 9257 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 𝑆 ∈ V) → (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃)) |
102 | 94, 100, 101 | mp2an 704 |
. . . . 5
⊢ (𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃) |
103 | 102 | biimpri 217 |
. . . 4
⊢ (¬
𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆) |
104 | | fodomr 7996 |
. . . 4
⊢ ((∅
≺ 𝑃 ∧ 𝑃 ≼ 𝑆) → ∃𝑓 𝑓:𝑆–onto→𝑃) |
105 | 98, 103, 104 | syl2an 493 |
. . 3
⊢
((∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) ∧ ¬ 𝑆 ≺ 𝑃) → ∃𝑓 𝑓:𝑆–onto→𝑃) |
106 | 83, 105 | mtand 689 |
. 2
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → ¬ ¬ 𝑆 ≺ 𝑃) |
107 | 106 | notnotrd 127 |
1
⊢
(∀𝑖 ∈
𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃) |