Metamath Proof Explorer

Theorem symg2bas

Description: The symmetric group on a pair is the symmetric group S_2 consisting of the identity and the transposition. Notice that this statement is valid for proper pairs only. In the case that both elements are identical, i.e., the pairs are actually singletons, this theorem would be about S_1, see Theorem symg1bas . (Contributed by AV, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

Ref Expression
Hypotheses symg1bas.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symg1bas.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
symg2bas.0 ⊢ 𝐴 = { 𝐼 , 𝐽 }
Assertion symg2bas ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } )

Proof

Step Hyp Ref Expression
1 symg1bas.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 symg1bas.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 symg2bas.0 ⊢ 𝐴 = { 𝐼 , 𝐽 }
4 eqid ⊢ ( SymGrp ‘ { 𝐽 } ) = ( SymGrp ‘ { 𝐽 } )
5 eqid ⊢ ( Base ‘ ( SymGrp ‘ { 𝐽 } ) ) = ( Base ‘ ( SymGrp ‘ { 𝐽 } ) )
6 eqid ⊢ { 𝐽 } = { 𝐽 }
7 4 5 6 symg1bas ⊢ ( 𝐽 ∈ 𝑊 → ( Base ‘ ( SymGrp ‘ { 𝐽 } ) ) = { { ⟨ 𝐽 , 𝐽 ⟩ } } )
8 7 ad2antll ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( Base ‘ ( SymGrp ‘ { 𝐽 } ) ) = { { ⟨ 𝐽 , 𝐽 ⟩ } } )
9 df-pr ⊢ { 𝐼 , 𝐽 } = ( { 𝐼 } ∪ { 𝐽 } )
10 sneq ⊢ ( 𝐼 = 𝐽 → { 𝐼 } = { 𝐽 } )
11 10 uneq1d ⊢ ( 𝐼 = 𝐽 → ( { 𝐼 } ∪ { 𝐽 } ) = ( { 𝐽 } ∪ { 𝐽 } ) )
12 11 adantr ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( { 𝐼 } ∪ { 𝐽 } ) = ( { 𝐽 } ∪ { 𝐽 } ) )
13 unidm ⊢ ( { 𝐽 } ∪ { 𝐽 } ) = { 𝐽 }
14 12 13 eqtrdi ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( { 𝐼 } ∪ { 𝐽 } ) = { 𝐽 } )
15 9 14 eqtrid ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { 𝐼 , 𝐽 } = { 𝐽 } )
16 3 15 eqtrid ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → 𝐴 = { 𝐽 } )
17 16 fveq2d ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( SymGrp ‘ 𝐴 ) = ( SymGrp ‘ { 𝐽 } ) )
18 1 17 eqtrid ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → 𝐺 = ( SymGrp ‘ { 𝐽 } ) )
19 18 fveq2d ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( Base ‘ 𝐺 ) = ( Base ‘ ( SymGrp ‘ { 𝐽 } ) ) )
20 2 19 eqtrid ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → 𝐵 = ( Base ‘ ( SymGrp ‘ { 𝐽 } ) ) )
21 id ⊢ ( 𝐼 = 𝐽 → 𝐼 = 𝐽 )
22 21 21 opeq12d ⊢ ( 𝐼 = 𝐽 → ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐽 , 𝐽 ⟩ )
23 22 adantr ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐽 , 𝐽 ⟩ )
24 23 preq1d ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } )
25 eqid ⊢ ⟨ 𝐽 , 𝐽 ⟩ = ⟨ 𝐽 , 𝐽 ⟩
26 opex ⊢ ⟨ 𝐽 , 𝐽 ⟩ ∈ V
27 26 26 preqsn ⊢ ( { ⟨ 𝐽 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ } ↔ ( ⟨ 𝐽 , 𝐽 ⟩ = ⟨ 𝐽 , 𝐽 ⟩ ∧ ⟨ 𝐽 , 𝐽 ⟩ = ⟨ 𝐽 , 𝐽 ⟩ ) )
28 25 25 27 mpbir2an ⊢ { ⟨ 𝐽 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ }
29 24 28 eqtrdi ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ } )
30 opeq1 ⊢ ( 𝐼 = 𝐽 → ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝐽 , 𝐽 ⟩ )
31 opeq2 ⊢ ( 𝐼 = 𝐽 → ⟨ 𝐽 , 𝐼 ⟩ = ⟨ 𝐽 , 𝐽 ⟩ )
32 30 31 preq12d ⊢ ( 𝐼 = 𝐽 → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } )
33 32 28 eqtrdi ⊢ ( 𝐼 = 𝐽 → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ } )
34 33 adantr ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ } )
35 29 34 preq12d ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } = { { ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐽 , 𝐽 ⟩ } } )
36 eqid ⊢ { ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ }
37 snex ⊢ { ⟨ 𝐽 , 𝐽 ⟩ } ∈ V
38 37 37 preqsn ⊢ ( { { ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐽 , 𝐽 ⟩ } } = { { ⟨ 𝐽 , 𝐽 ⟩ } } ↔ ( { ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ } ∧ { ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐽 , 𝐽 ⟩ } ) )
39 36 36 38 mpbir2an ⊢ { { ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐽 , 𝐽 ⟩ } } = { { ⟨ 𝐽 , 𝐽 ⟩ } }
40 35 39 eqtrdi ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } = { { ⟨ 𝐽 , 𝐽 ⟩ } } )
41 8 20 40 3eqtr4d ⊢ ( ( 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } )
42 2 fvexi ⊢ 𝐵 ∈ V
43 42 a1i ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → 𝐵 ∈ V )
44 neqne ⊢ ( ¬ 𝐼 = 𝐽 → 𝐼 ≠ 𝐽 )
45 44 anim2i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ∧ ¬ 𝐼 = 𝐽 ) → ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ∧ 𝐼 ≠ 𝐽 ) )
46 df-3an ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) ↔ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ∧ 𝐼 ≠ 𝐽 ) )
47 45 46 sylibr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ∧ ¬ 𝐼 = 𝐽 ) → ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) )
48 47 ancoms ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) )
49 1 2 3 symg2hash ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐵 ) = 2 )
50 48 49 syl ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( ♯ ‘ 𝐵 ) = 2 )
51 id ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉 )
52 51 ancri ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) )
53 id ⊢ ( 𝐽 ∈ 𝑊 → 𝐽 ∈ 𝑊 )
54 53 ancri ⊢ ( 𝐽 ∈ 𝑊 → ( 𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊 ) )
55 52 54 anim12i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊 ) ) )
56 df-ne ⊢ ( 𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽 )
57 id ⊢ ( 𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽 )
58 57 ancri ⊢ ( 𝐼 ≠ 𝐽 → ( 𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽 ) )
59 56 58 sylbir ⊢ ( ¬ 𝐼 = 𝐽 → ( 𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽 ) )
60 f1oprg ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊 ) ) → ( ( 𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽 ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
61 60 imp ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊 ) ) ∧ ( 𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } )
62 55 59 61 syl2anr ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } )
63 eqidd ⊢ ( 𝐴 = { 𝐼 , 𝐽 } → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } = { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } )
64 id ⊢ ( 𝐴 = { 𝐼 , 𝐽 } → 𝐴 = { 𝐼 , 𝐽 } )
65 63 64 64 f1oeq123d ⊢ ( 𝐴 = { 𝐼 , 𝐽 } → ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : 𝐴 –1-1-onto→ 𝐴 ↔ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
66 3 65 ax-mp ⊢ ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : 𝐴 –1-1-onto→ 𝐴 ↔ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } )
67 62 66 sylibr ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : 𝐴 –1-1-onto→ 𝐴 )
68 prex ⊢ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ V
69 1 2 elsymgbas2 ⊢ ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ V → ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ 𝐵 ↔ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : 𝐴 –1-1-onto→ 𝐴 ) )
70 68 69 ax-mp ⊢ ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ 𝐵 ↔ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } : 𝐴 –1-1-onto→ 𝐴 )
71 67 70 sylibr ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ 𝐵 )
72 f1oprswap ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } )
73 eqidd ⊢ ( 𝐴 = { 𝐼 , 𝐽 } → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } = { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } )
74 73 64 64 f1oeq123d ⊢ ( 𝐴 = { 𝐼 , 𝐽 } → ( { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : 𝐴 –1-1-onto→ 𝐴 ↔ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } ) )
75 3 74 ax-mp ⊢ ( { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : 𝐴 –1-1-onto→ 𝐴 ↔ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : { 𝐼 , 𝐽 } –1-1-onto→ { 𝐼 , 𝐽 } )
76 72 75 sylibr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : 𝐴 –1-1-onto→ 𝐴 )
77 76 adantl ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : 𝐴 –1-1-onto→ 𝐴 )
78 prex ⊢ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ V
79 1 2 elsymgbas2 ⊢ ( { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ V → ( { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ 𝐵 ↔ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : 𝐴 –1-1-onto→ 𝐴 ) )
80 78 79 ax-mp ⊢ ( { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ 𝐵 ↔ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } : 𝐴 –1-1-onto→ 𝐴 )
81 77 80 sylibr ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ 𝐵 )
82 opex ⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
83 82 26 pm3.2i ⊢ ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ ⟨ 𝐽 , 𝐽 ⟩ ∈ V )
84 opex ⊢ ⟨ 𝐼 , 𝐽 ⟩ ∈ V
85 opex ⊢ ⟨ 𝐽 , 𝐼 ⟩ ∈ V
86 84 85 pm3.2i ⊢ ( ⟨ 𝐼 , 𝐽 ⟩ ∈ V ∧ ⟨ 𝐽 , 𝐼 ⟩ ∈ V )
87 83 86 pm3.2i ⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ ⟨ 𝐽 , 𝐽 ⟩ ∈ V ) ∧ ( ⟨ 𝐼 , 𝐽 ⟩ ∈ V ∧ ⟨ 𝐽 , 𝐼 ⟩ ∈ V ) )
88 opthg2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐼 , 𝐽 ⟩ ↔ ( 𝐼 = 𝐼 ∧ 𝐼 = 𝐽 ) ) )
89 eqtr ⊢ ( ( 𝐼 = 𝐼 ∧ 𝐼 = 𝐽 ) → 𝐼 = 𝐽 )
90 88 89 biimtrdi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐼 , 𝐽 ⟩ → 𝐼 = 𝐽 ) )
91 90 necon3d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( 𝐼 ≠ 𝐽 → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ) )
92 91 com12 ⊢ ( 𝐼 ≠ 𝐽 → ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ) )
93 56 92 sylbir ⊢ ( ¬ 𝐼 = 𝐽 → ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ) )
94 93 imp ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ )
95 52 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) )
96 opthg ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) → ( ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐽 , 𝐼 ⟩ ↔ ( 𝐼 = 𝐽 ∧ 𝐼 = 𝐼 ) ) )
97 95 96 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐽 , 𝐼 ⟩ ↔ ( 𝐼 = 𝐽 ∧ 𝐼 = 𝐼 ) ) )
98 simpl ⊢ ( ( 𝐼 = 𝐽 ∧ 𝐼 = 𝐼 ) → 𝐼 = 𝐽 )
99 97 98 biimtrdi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( ⟨ 𝐼 , 𝐼 ⟩ = ⟨ 𝐽 , 𝐼 ⟩ → 𝐼 = 𝐽 ) )
100 99 necon3d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ( 𝐼 ≠ 𝐽 → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) )
101 100 com12 ⊢ ( 𝐼 ≠ 𝐽 → ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) )
102 56 101 sylbir ⊢ ( ¬ 𝐼 = 𝐽 → ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) )
103 102 imp ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ )
104 94 103 jca ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ∧ ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) )
105 104 orcd ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → ( ( ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ∧ ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) ∨ ( ⟨ 𝐽 , 𝐽 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ∧ ⟨ 𝐽 , 𝐽 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) ) )
106 prneimg ⊢ ( ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ ⟨ 𝐽 , 𝐽 ⟩ ∈ V ) ∧ ( ⟨ 𝐼 , 𝐽 ⟩ ∈ V ∧ ⟨ 𝐽 , 𝐼 ⟩ ∈ V ) ) → ( ( ( ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ∧ ⟨ 𝐼 , 𝐼 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) ∨ ( ⟨ 𝐽 , 𝐽 ⟩ ≠ ⟨ 𝐼 , 𝐽 ⟩ ∧ ⟨ 𝐽 , 𝐽 ⟩ ≠ ⟨ 𝐽 , 𝐼 ⟩ ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ≠ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ) )
107 87 105 106 mpsyl ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ≠ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } )
108 hash2prd ⊢ ( ( 𝐵 ∈ V ∧ ( ♯ ‘ 𝐵 ) = 2 ) → ( ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ 𝐵 ∧ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ 𝐵 ∧ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ≠ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ) → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } ) )
109 108 imp ⊢ ( ( ( 𝐵 ∈ V ∧ ( ♯ ‘ 𝐵 ) = 2 ) ∧ ( { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ∈ 𝐵 ∧ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ∈ 𝐵 ∧ { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } ≠ { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } ) ) → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } )
110 43 50 71 81 107 109 syl23anc ⊢ ( ( ¬ 𝐼 = 𝐽 ∧ ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) ) → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } )
111 41 110 pm2.61ian ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ) → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ , ⟨ 𝐽 , 𝐽 ⟩ } , { ⟨ 𝐼 , 𝐽 ⟩ , ⟨ 𝐽 , 𝐼 ⟩ } } )