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 𝐶 , 𝐷 ( 𝐴 , 𝐵 ) )