This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem konigthlem

Description: Lemma for konigth . (Contributed by Mario Carneiro, 22-Feb-2013)

Ref Expression
Hypotheses konigth.1 ⊢ 𝐴 ∈ V
konigth.2 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 )
konigth.3 ⊢ 𝑃 = X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 )
konigth.4 ⊢ 𝐷 = ( 𝑖 ∈ 𝐴 ↦ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) )
konigth.5 ⊢ 𝐸 = ( 𝑖 ∈ 𝐴 ↦ ( 𝑒 ‘ 𝑖 ) )
Assertion konigthlem ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → 𝑆 ≺ 𝑃 )

Proof

Step Hyp Ref Expression
1 konigth.1 ⊢ 𝐴 ∈ V
2 konigth.2 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 )
3 konigth.3 ⊢ 𝑃 = X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 )
4 konigth.4 ⊢ 𝐷 = ( 𝑖 ∈ 𝐴 ↦ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) )
5 konigth.5 ⊢ 𝐸 = ( 𝑖 ∈ 𝐴 ↦ ( 𝑒 ‘ 𝑖 ) )
6 fvex ⊢ ( 𝑀 ‘ 𝑖 ) ∈ V
7 fvex ⊢ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ∈ V
8 eqid ⊢ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) = ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
9 7 8 fnmpti ⊢ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) Fn ( 𝑀 ‘ 𝑖 )
10 6 mptex ⊢ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) ∈ V
11 4 fvmpt2 ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) ∈ V ) → ( 𝐷 ‘ 𝑖 ) = ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) )
12 10 11 mpan2 ⊢ ( 𝑖 ∈ 𝐴 → ( 𝐷 ‘ 𝑖 ) = ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) )
13 12 fneq1d ⊢ ( 𝑖 ∈ 𝐴 → ( ( 𝐷 ‘ 𝑖 ) Fn ( 𝑀 ‘ 𝑖 ) ↔ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) Fn ( 𝑀 ‘ 𝑖 ) ) )
14 9 13 mpbiri ⊢ ( 𝑖 ∈ 𝐴 → ( 𝐷 ‘ 𝑖 ) Fn ( 𝑀 ‘ 𝑖 ) )
15 fnrndomg ⊢ ( ( 𝑀 ‘ 𝑖 ) ∈ V → ( ( 𝐷 ‘ 𝑖 ) Fn ( 𝑀 ‘ 𝑖 ) → ran ( 𝐷 ‘ 𝑖 ) ≼ ( 𝑀 ‘ 𝑖 ) ) )
16 6 14 15 mpsyl ⊢ ( 𝑖 ∈ 𝐴 → ran ( 𝐷 ‘ 𝑖 ) ≼ ( 𝑀 ‘ 𝑖 ) )
17 domsdomtr ⊢ ( ( ran ( 𝐷 ‘ 𝑖 ) ≼ ( 𝑀 ‘ 𝑖 ) ∧ ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) ) → ran ( 𝐷 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) )
18 16 17 sylan ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) ) → ran ( 𝐷 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) )
19 sdomdif ⊢ ( ran ( 𝐷 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ≠ ∅ )
20 18 19 syl ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) ) → ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ≠ ∅ )
21 20 ralimiaa ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ∀ 𝑖 ∈ 𝐴 ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ≠ ∅ )
22 fvex ⊢ ( 𝑁 ‘ 𝑖 ) ∈ V
23 22 difexi ⊢ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∈ V
24 1 23 ac6c5 ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ≠ ∅ → ∃ 𝑒 ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) )
25 equid ⊢ 𝑓 = 𝑓
26 eldifi ⊢ ( ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝑒 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) )
27 fvex ⊢ ( 𝑒 ‘ 𝑖 ) ∈ V
28 5 fvmpt2 ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑒 ‘ 𝑖 ) ∈ V ) → ( 𝐸 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
29 27 28 mpan2 ⊢ ( 𝑖 ∈ 𝐴 → ( 𝐸 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
30 29 eleq1d ⊢ ( 𝑖 ∈ 𝐴 → ( ( 𝐸 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) ↔ ( 𝑒 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) ) )
31 26 30 imbitrrid ⊢ ( 𝑖 ∈ 𝐴 → ( ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝐸 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) ) )
32 31 ralimia ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ 𝐴 ( 𝐸 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) )
33 27 5 fnmpti ⊢ 𝐸 Fn 𝐴
34 32 33 jctil ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝐸 Fn 𝐴 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐸 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) ) )
35 1 mptex ⊢ ( 𝑖 ∈ 𝐴 ↦ ( 𝑒 ‘ 𝑖 ) ) ∈ V
36 5 35 eqeltri ⊢ 𝐸 ∈ V
37 36 elixp ⊢ ( 𝐸 ∈ X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ↔ ( 𝐸 Fn 𝐴 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐸 ‘ 𝑖 ) ∈ ( 𝑁 ‘ 𝑖 ) ) )
38 34 37 sylibr ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → 𝐸 ∈ X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) )
39 38 3 eleqtrrdi ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → 𝐸 ∈ 𝑃 )
40 foelrn ⊢ ( ( 𝑓 : 𝑆 –onto→ 𝑃 ∧ 𝐸 ∈ 𝑃 ) → ∃ 𝑎 ∈ 𝑆 𝐸 = ( 𝑓 ‘ 𝑎 ) )
41 40 expcom ⊢ ( 𝐸 ∈ 𝑃 → ( 𝑓 : 𝑆 –onto→ 𝑃 → ∃ 𝑎 ∈ 𝑆 𝐸 = ( 𝑓 ‘ 𝑎 ) ) )
42 2 eleq2i ⊢ ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) )
43 eliun ⊢ ( 𝑎 ∈ ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ 𝐴 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) )
44 42 43 bitri ⊢ ( 𝑎 ∈ 𝑆 ↔ ∃ 𝑖 ∈ 𝐴 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) )
45 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) )
46 nfv ⊢ Ⅎ 𝑖 𝐸 = ( 𝑓 ‘ 𝑎 )
47 45 46 nfan ⊢ Ⅎ 𝑖 ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) )
48 nfv ⊢ Ⅎ 𝑖 ¬ 𝑓 = 𝑓
49 29 ad2antrl ⊢ ( ( 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ( 𝐸 ‘ 𝑖 ) = ( 𝑒 ‘ 𝑖 ) )
50 fveq1 ⊢ ( 𝐸 = ( 𝑓 ‘ 𝑎 ) → ( 𝐸 ‘ 𝑖 ) = ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
51 12 fveq1d ⊢ ( 𝑖 ∈ 𝐴 → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) = ( ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) ‘ 𝑎 ) )
52 8 fvmpt2 ⊢ ( ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ∧ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ∈ V ) → ( ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) ‘ 𝑎 ) = ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
53 7 52 mpan2 ⊢ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) → ( ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) ‘ 𝑎 ) = ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
54 51 53 sylan9eq ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) = ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
55 54 eqcomd ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) → ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) )
56 50 55 sylan9eq ⊢ ( ( 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ( 𝐸 ‘ 𝑖 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) )
57 49 56 eqtr3d ⊢ ( ( 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ( 𝑒 ‘ 𝑖 ) = ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) )
58 fnfvelrn ⊢ ( ( ( 𝐷 ‘ 𝑖 ) Fn ( 𝑀 ‘ 𝑖 ) ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
59 14 58 sylan ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
60 59 adantl ⊢ ( ( 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑎 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
61 57 60 eqeltrd ⊢ ( ( 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ( 𝑒 ‘ 𝑖 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
62 61 3adant1 ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ( 𝑒 ‘ 𝑖 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
63 simp1 ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) )
64 simp3l ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → 𝑖 ∈ 𝐴 )
65 rsp ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝑖 ∈ 𝐴 → ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ) )
66 eldifn ⊢ ( ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ¬ ( 𝑒 ‘ 𝑖 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
67 65 66 syl6 ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝑖 ∈ 𝐴 → ¬ ( 𝑒 ‘ 𝑖 ) ∈ ran ( 𝐷 ‘ 𝑖 ) ) )
68 63 64 67 sylc ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ¬ ( 𝑒 ‘ 𝑖 ) ∈ ran ( 𝐷 ‘ 𝑖 ) )
69 62 68 pm2.21dd ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) ) → ¬ 𝑓 = 𝑓 )
70 69 3expia ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ) → ¬ 𝑓 = 𝑓 ) )
71 70 expd ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ) → ( 𝑖 ∈ 𝐴 → ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) → ¬ 𝑓 = 𝑓 ) ) )
72 47 48 71 rexlimd ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ) → ( ∃ 𝑖 ∈ 𝐴 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) → ¬ 𝑓 = 𝑓 ) )
73 44 72 biimtrid ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) ∧ 𝐸 = ( 𝑓 ‘ 𝑎 ) ) → ( 𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓 ) )
74 73 ex ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝐸 = ( 𝑓 ‘ 𝑎 ) → ( 𝑎 ∈ 𝑆 → ¬ 𝑓 = 𝑓 ) ) )
75 74 com23 ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝑎 ∈ 𝑆 → ( 𝐸 = ( 𝑓 ‘ 𝑎 ) → ¬ 𝑓 = 𝑓 ) ) )
76 75 rexlimdv ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( ∃ 𝑎 ∈ 𝑆 𝐸 = ( 𝑓 ‘ 𝑎 ) → ¬ 𝑓 = 𝑓 ) )
77 41 76 syl9r ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝐸 ∈ 𝑃 → ( 𝑓 : 𝑆 –onto→ 𝑃 → ¬ 𝑓 = 𝑓 ) ) )
78 39 77 mpd ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ( 𝑓 : 𝑆 –onto→ 𝑃 → ¬ 𝑓 = 𝑓 ) )
79 25 78 mt2i ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ¬ 𝑓 : 𝑆 –onto→ 𝑃 )
80 79 exlimiv ⊢ ( ∃ 𝑒 ∀ 𝑖 ∈ 𝐴 ( 𝑒 ‘ 𝑖 ) ∈ ( ( 𝑁 ‘ 𝑖 ) ∖ ran ( 𝐷 ‘ 𝑖 ) ) → ¬ 𝑓 : 𝑆 –onto→ 𝑃 )
81 21 24 80 3syl ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ¬ 𝑓 : 𝑆 –onto→ 𝑃 )
82 81 nexdv ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ¬ ∃ 𝑓 𝑓 : 𝑆 –onto→ 𝑃 )
83 6 0dom ⊢ ∅ ≼ ( 𝑀 ‘ 𝑖 )
84 domsdomtr ⊢ ( ( ∅ ≼ ( 𝑀 ‘ 𝑖 ) ∧ ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) ) → ∅ ≺ ( 𝑁 ‘ 𝑖 ) )
85 83 84 mpan ⊢ ( ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ∅ ≺ ( 𝑁 ‘ 𝑖 ) )
86 22 0sdom ⊢ ( ∅ ≺ ( 𝑁 ‘ 𝑖 ) ↔ ( 𝑁 ‘ 𝑖 ) ≠ ∅ )
87 85 86 sylib ⊢ ( ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ( 𝑁 ‘ 𝑖 ) ≠ ∅ )
88 87 ralimi ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ∀ 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ≠ ∅ )
89 3 neeq1i ⊢ ( 𝑃 ≠ ∅ ↔ X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ≠ ∅ )
90 22 rgenw ⊢ ∀ 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ∈ V
91 ixpexg ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ∈ V → X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ∈ V )
92 90 91 ax-mp ⊢ X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ∈ V
93 3 92 eqeltri ⊢ 𝑃 ∈ V
94 93 0sdom ⊢ ( ∅ ≺ 𝑃 ↔ 𝑃 ≠ ∅ )
95 1 22 ac9 ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ≠ ∅ ↔ X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ≠ ∅ )
96 89 94 95 3bitr4i ⊢ ( ∅ ≺ 𝑃 ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 ) ≠ ∅ )
97 88 96 sylibr ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ∅ ≺ 𝑃 )
98 1 6 iunex ⊢ ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ∈ V
99 2 98 eqeltri ⊢ 𝑆 ∈ V
100 domtri ⊢ ( ( 𝑃 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃 ) )
101 93 99 100 mp2an ⊢ ( 𝑃 ≼ 𝑆 ↔ ¬ 𝑆 ≺ 𝑃 )
102 101 biimpri ⊢ ( ¬ 𝑆 ≺ 𝑃 → 𝑃 ≼ 𝑆 )
103 fodomr ⊢ ( ( ∅ ≺ 𝑃 ∧ 𝑃 ≼ 𝑆 ) → ∃ 𝑓 𝑓 : 𝑆 –onto→ 𝑃 )
104 97 102 103 syl2an ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) ∧ ¬ 𝑆 ≺ 𝑃 ) → ∃ 𝑓 𝑓 : 𝑆 –onto→ 𝑃 )
105 82 104 mtand ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → ¬ ¬ 𝑆 ≺ 𝑃 )
106 105 notnotrd ⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → 𝑆 ≺ 𝑃 )