Metamath Proof Explorer

Theorem isocnv3

Description: Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses isocnv3.1 ⊢ 𝐶 = ( ( 𝐴 × 𝐴 ) ∖ 𝑅 )
isocnv3.2 ⊢ 𝐷 = ( ( 𝐵 × 𝐵 ) ∖ 𝑆 )
Assertion isocnv3 ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝐶 , 𝐷 ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 isocnv3.1 ⊢ 𝐶 = ( ( 𝐴 × 𝐴 ) ∖ 𝑅 )
2 isocnv3.2 ⊢ 𝐷 = ( ( 𝐵 × 𝐵 ) ∖ 𝑆 )
3 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
4 1 breqi ⊢ ( 𝑥 𝐶 𝑦 ↔ 𝑥 ( ( 𝐴 × 𝐴 ) ∖ 𝑅 ) 𝑦 )
5 brdif ⊢ ( 𝑥 ( ( 𝐴 × 𝐴 ) ∖ 𝑅 ) 𝑦 ↔ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ ¬ 𝑥 𝑅 𝑦 ) )
6 4 5 bitri ⊢ ( 𝑥 𝐶 𝑦 ↔ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ ¬ 𝑥 𝑅 𝑦 ) )
7 6 baib ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 → ( 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
8 3 7 sylbir ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
9 8 adantl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
10 f1of ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
11 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
12 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 )
13 11 12 anim12dan ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) )
14 brxp ⊢ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) )
15 13 14 sylibr ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) )
16 10 15 sylan ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) )
17 2 breqi ⊢ ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) ( ( 𝐵 × 𝐵 ) ∖ 𝑆 ) ( 𝐻 ‘ 𝑦 ) )
18 brdif ⊢ ( ( 𝐻 ‘ 𝑥 ) ( ( 𝐵 × 𝐵 ) ∖ 𝑆 ) ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) ∧ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
19 17 18 bitri ⊢ ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) ∧ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
20 19 baib ⊢ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) → ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
21 16 20 syl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
22 9 21 bibi12d ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝐶 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
23 notbi ⊢ ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
24 22 23 syl6rbbr ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑥 𝐶 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ) ) )
25 24 2ralbidva ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐶 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ) ) )
26 25 pm5.32i ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐶 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ) ) )
27 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
28 df-isom ⊢ ( 𝐻 Isom 𝐶 , 𝐷 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝐶 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ) ) )
29 26 27 28 3bitr4i ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝐶 , 𝐷 ( 𝐴 , 𝐵 ) )