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 notbi ⊢ ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
4 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
5 1 breqi ⊢ ( 𝑥 𝐶 𝑦 ↔ 𝑥 ( ( 𝐴 × 𝐴 ) ∖ 𝑅 ) 𝑦 )
6 brdif ⊢ ( 𝑥 ( ( 𝐴 × 𝐴 ) ∖ 𝑅 ) 𝑦 ↔ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ ¬ 𝑥 𝑅 𝑦 ) )
7 5 6 bitri ⊢ ( 𝑥 𝐶 𝑦 ↔ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ ¬ 𝑥 𝑅 𝑦 ) )
8 7 baib ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 → ( 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
9 4 8 sylbir ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
10 9 adantl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
11 f1of ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
12 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
13 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 )
14 12 13 anim12dan ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) )
15 brxp ⊢ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) )
16 14 15 sylibr ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) )
17 11 16 sylan ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) )
18 2 breqi ⊢ ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) ( ( 𝐵 × 𝐵 ) ∖ 𝑆 ) ( 𝐻 ‘ 𝑦 ) )
19 brdif ⊢ ( ( 𝐻 ‘ 𝑥 ) ( ( 𝐵 × 𝐵 ) ∖ 𝑆 ) ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) ∧ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
20 18 19 bitri ⊢ ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) ∧ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
21 20 baib ⊢ ( ( 𝐻 ‘ 𝑥 ) ( 𝐵 × 𝐵 ) ( 𝐻 ‘ 𝑦 ) → ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
22 17 21 syl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
23 10 22 bibi12d ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝐶 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝐷 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
24 3 23 bitr4id ⊢ ( ( 𝐻 : 𝐴 –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 𝐶 , 𝐷 ( 𝐴 , 𝐵 ) )