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 elun ⊢ ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↔ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏 ) )
24 23 bilani ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → ( 𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏 ) )
25 24 orcanai ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ ¬ 𝑥 ∈ 𝑎 ) → 𝑥 ∈ 𝑏 )
26 22 25 opelxpd ⊢ ( ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) ∧ ¬ 𝑥 ∈ 𝑎 ) → ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ ∈ ( 𝑎 × 𝑏 ) )
27 18 26 ifclda ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ ) ∈ ( 𝑎 × 𝑏 ) )
28 2 27 eqeltrid ⊢ ( ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) ∧ 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝐺 ∈ ( 𝑎 × 𝑏 ) )
29 28 1 fmptd ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝐹 : ( 𝑎 ∪ 𝑏 ) ⟶ ( 𝑎 × 𝑏 ) )
30 1 2 unxpdomlem1 ⊢ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
31 30 ad2antrl ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
32 iftrue ⊢ ( 𝑧 ∈ 𝑎 → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
33 32 adantr ⊢ ( ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
34 31 33 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
35 1 2 unxpdomlem1 ⊢ ( 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑤 ) = if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
36 35 ad2antll ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ( 𝐹 ‘ 𝑤 ) = if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
37 iftrue ⊢ ( 𝑤 ∈ 𝑎 → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
38 37 adantl ⊢ ( ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
39 36 38 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑤 ) = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
40 34 39 eqeq12d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ ) )
41 vex ⊢ 𝑧 ∈ V
42 vex ⊢ 𝑡 ∈ V
43 vex ⊢ 𝑠 ∈ V
44 42 43 ifex ⊢ if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ∈ V
45 41 44 opth1 ⊢ ( ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ → 𝑧 = 𝑤 )
46 40 45 biimtrdi ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
47 simprr ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) )
48 simpll ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ¬ 𝑚 = 𝑛 )
49 simplr ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ¬ 𝑠 = 𝑡 )
50 1 2 47 48 49 unxpdomlem2 ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
51 50 pm2.21d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
52 eqcom ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
53 simprl ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) )
54 1 2 53 48 49 unxpdomlem2 ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( 𝑤 ∈ 𝑎 ∧ ¬ 𝑧 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
55 54 ancom2s ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
56 55 pm2.21d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) → 𝑧 = 𝑤 ) )
57 52 56 biimtrid ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
58 iffalse ⊢ ( ¬ 𝑧 ∈ 𝑎 → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
59 58 adantr ⊢ ( ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
60 31 59 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
61 iffalse ⊢ ( ¬ 𝑤 ∈ 𝑎 → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
62 61 adantl ⊢ ( ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
63 36 62 sylan9eq ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑤 ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
64 60 63 eqeq12d ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
65 vex ⊢ 𝑛 ∈ V
66 vex ⊢ 𝑚 ∈ V
67 65 66 ifex ⊢ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) ∈ V
68 67 41 opth ⊢ ( ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ↔ ( if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) = if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) ∧ 𝑧 = 𝑤 ) )
69 68 simprbi ⊢ ( ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ → 𝑧 = 𝑤 )
70 64 69 biimtrdi ⊢ ( ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) ∧ ( ¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
71 46 51 57 70 4casesdan ⊢ ( ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ∧ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∧ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
72 71 ralrimivva ⊢ ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) → ∀ 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∀ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
73 72 3ad2ant3 ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → ∀ 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∀ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
74 dff13 ⊢ ( 𝐹 : ( 𝑎 ∪ 𝑏 ) –1-1→ ( 𝑎 × 𝑏 ) ↔ ( 𝐹 : ( 𝑎 ∪ 𝑏 ) ⟶ ( 𝑎 × 𝑏 ) ∧ ∀ 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) ∀ 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
75 29 73 74 sylanbrc ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → 𝐹 : ( 𝑎 ∪ 𝑏 ) –1-1→ ( 𝑎 × 𝑏 ) )
76 f1dom2g ⊢ ( ( ( 𝑎 ∪ 𝑏 ) ∈ V ∧ ( 𝑎 × 𝑏 ) ∈ V ∧ 𝐹 : ( 𝑎 ∪ 𝑏 ) –1-1→ ( 𝑎 × 𝑏 ) ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
77 11 12 75 76 mp3an12i ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ∧ ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
78 77 3expia ⊢ ( ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) ∧ ( 𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏 ) ) → ( ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) ) )
79 78 rexlimdvva ⊢ ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) → ( ∃ 𝑛 ∈ 𝑎 ∃ 𝑡 ∈ 𝑏 ( ¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) ) )
80 8 79 biimtrrid ⊢ ( ( 𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏 ) → ( ( ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) ) )
81 80 rexlimivv ⊢ ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑠 ∈ 𝑏 ( ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
82 7 81 sylbir ⊢ ( ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃ 𝑠 ∈ 𝑏 ∃ 𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )
83 4 6 82 syl2anb ⊢ ( ( 1o ≺ 𝑎 ∧ 1o ≺ 𝑏 ) → ( 𝑎 ∪ 𝑏 ) ≼ ( 𝑎 × 𝑏 ) )