Metamath Proof Explorer

Theorem unxpdomlem3

Description: Lemma for unxpdom . (Contributed by Mario Carneiro, 13-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypotheses unxpdomlem1.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↦ 𝐺 )
unxpdomlem1.2 ⊢ 𝐺 = if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ )
Assertion unxpdomlem3 ( ( 1o ≺ 𝑎 ∧ 1o ≺ 𝑏 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )

Proof

Step Hyp Ref Expression
1 unxpdomlem1.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↦ 𝐺 )
2 unxpdomlem1.2 ⊢ 𝐺 = if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ )
3 1sdom ⊢ ( 𝑎 ∈ V → ( 1o ≺ 𝑎 ↔ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ) )
4 3 elv ⊢ ( 1o ≺ 𝑎 ↔ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 )
5 1sdom ⊢ ( 𝑏 ∈ V → ( 1o ≺ 𝑏 ↔ ∃ 𝑠 ∈ 𝑏 ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) )
6 5 elv ⊢ ( 1o ≺ 𝑏 ↔ ∃ 𝑠 ∈ 𝑏 ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 )
7 reeanv ⊢ ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑠 ∈ 𝑏 ( ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) ↔ ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑠 ∈ 𝑏 ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) )
8 reeanv ⊢ ( ∃ 𝑛 ∈ 𝑎 ∃ 𝑡 ∈ 𝑏 ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ↔ ( ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) )
9 vex ⊢ 𝑎 ∈ V
10 vex ⊢ 𝑏 ∈ V
11 9 10 unex ⊢ ( 𝑎 ∪ 𝑏 ) ∈ V
12 9 10 xpex ⊢ ( 𝑎 × 𝑏 ) ∈ V
13 simpr ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ 𝑥 ∈ 𝑎 ) → 𝑥 ∈ 𝑎 )
14 simp2r ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝑡 ∈ 𝑏 )
15 simp1r ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝑠 ∈ 𝑏 )
16 14 15 ifcld ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ∈ 𝑏 )
17 16 ad2antrr ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ 𝑥 ∈ 𝑎 ) → if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ∈ 𝑏 )
18 13 17 opelxpd ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ 𝑥 ∈ 𝑎 ) → ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ ∈ ( 𝑎 × 𝑏 ) )
19 simp2l ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝑛 ∈ 𝑎 )
20 simp1l ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝑚 ∈ 𝑎 )
21 19 20 ifcld ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) ∈ 𝑎 )
22 21 ad2antrr ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ ¬ 𝑥 ∈ 𝑎 ) → if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) ∈ 𝑎 )
23 simpr ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) )
24 elun ⊢ ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↔ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏 ) )
25 23 24 sylib ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → ( 𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏 ) )
26 25 orcanai ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ ¬ 𝑥 ∈ 𝑎 ) → 𝑥 ∈ 𝑏 )
27 22 26 opelxpd ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ ¬ 𝑥 ∈ 𝑎 ) → ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ ∈ ( 𝑎 × 𝑏 ) )
28 18 27 ifclda ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ ) ∈ ( 𝑎 × 𝑏 ) )
29 2 28 eqeltrid ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝐺 ∈ ( 𝑎 × 𝑏 ) )
30 29 1 fmptd ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝐹 : ( 𝑎 ∪ 𝑏 ) ⟶ ( 𝑎 × 𝑏 ) )
31 1 2 unxpdomlem1 ⊢ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
32 31 ad2antrl ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
33 iftrue ⊢ ( 𝑧 ∈ 𝑎 → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
34 33 adantr ⊢ ( ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
35 32 34 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
36 1 2 unxpdomlem1 ⊢ ( 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑤 ) = if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
37 36 ad2antll ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ( 𝐹 ‘ 𝑤 ) = if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
38 iftrue ⊢ ( 𝑤 ∈ 𝑎 → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
39 38 adantl ⊢ ( ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
40 37 39 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑤 ) = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
41 35 40 eqeq12d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ ) )
42 vex ⊢ 𝑧 ∈ V
43 vex ⊢ 𝑡 ∈ V
44 vex ⊢ 𝑠 ∈ V
45 43 44 ifex ⊢ if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ∈ V
46 42 45 opth1 ⊢ ( ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ → 𝑧 = 𝑤 )
47 41 46 syl6bi ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
48 simprr ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) )
49 simpll ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ¬ 𝑚 = 𝑛 )
50 simplr ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ¬ 𝑠 = 𝑡 )
51 1 2 48 49 50 unxpdomlem2 ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
52 51 pm2.21d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
53 eqcom ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
54 simprl ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) )
55 1 2 54 49 50 unxpdomlem2 ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑤 ∈ 𝑎 ∧ ¬ 𝑧 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
56 55 ancom2s ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
57 56 pm2.21d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) → 𝑧 = 𝑤 ) )
58 53 57 syl5bi ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
59 iffalse ⊢ ( ¬ 𝑧 ∈ 𝑎 → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
60 59 adantr ⊢ ( ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
61 32 60 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
62 iffalse ⊢ ( ¬ 𝑤 ∈ 𝑎 → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
63 62 adantl ⊢ ( ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
64 37 63 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑤 ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
65 61 64 eqeq12d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
66 vex ⊢ 𝑛 ∈ V
67 vex ⊢ 𝑚 ∈ V
68 66 67 ifex ⊢ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) ∈ V
69 68 42 opth ⊢ ( ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ↔ ( if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) = if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) ∧ 𝑧 = 𝑤 ) )
70 69 simprbi ⊢ ( ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ → 𝑧 = 𝑤 )
71 65 70 syl6bi ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
72 47 52 58 71 4casesdan ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
73 72 ralrimivva ⊢ ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) → ∀ 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∀ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
74 73 3ad2ant3 ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → ∀ 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∀ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
75 dff13 ⊢ ( 𝐹 : ( 𝑎 ∪ 𝑏 ) –1-1→ ( 𝑎 × 𝑏 ) ↔ ( 𝐹 : ( 𝑎 ∪ 𝑏 ) ⟶ ( 𝑎 × 𝑏 ) ∧ ∀ 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∀ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
76 30 74 75 sylanbrc ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝐹 : ( 𝑎 ∪ 𝑏 ) –1-1→ ( 𝑎 × 𝑏 ) )
77 f1dom2g ⊢ ( ( ( 𝑎 ∪ 𝑏 ) ∈ V ∧ ( 𝑎 × 𝑏 ) ∈ V ∧ 𝐹 : ( 𝑎 ∪ 𝑏 ) –1-1→ ( 𝑎 × 𝑏 ) ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
78 11 12 76 77 mp3an12i ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
79 78 3expia ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ) → ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) ) )
80 79 rexlimdvva ⊢ ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) → ( ∃ 𝑛 ∈ 𝑎 ∃ 𝑡 ∈ 𝑏 ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) ) )
81 8 80 syl5bir ⊢ ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) → ( ( ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) ) )
82 81 rexlimivv ⊢ ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑠 ∈ 𝑏 ( ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
83 7 82 sylbir ⊢ ( ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑠 ∈ 𝑏 ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
84 4 6 83 syl2anb ⊢ ( ( 1o ≺ 𝑎 ∧ 1o ≺ 𝑏 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )