This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isomin

Description: Isomorphisms preserve minimal elements. Note that (`' R " { D } ) ` is Takeuti and Zaring's idiom for the initial segment { x | x R D } . Proposition 6.31(1) of TakeutiZaring p. 33. (Contributed by NM, 19-Apr-2004)

Ref Expression
Assertion isomin ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 neq0 ⊢ ( ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
2 vex ⊢ 𝑦 ∈ V
3 2 elima ⊢ ( 𝑦 ∈ ( 𝐻 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 𝑥 𝐻 𝑦 )
4 ssel ⊢ ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) )
5 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
6 f1ofn ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Fn 𝐴 )
7 fnbrfvb ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐻 𝑦 ) )
8 7 ex ⊢ ( 𝐻 Fn 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐻 𝑦 ) ) )
9 5 6 8 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐻 𝑦 ) ) )
10 4 9 syl9r ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐻 𝑦 ) ) ) )
11 10 imp31 ⊢ ( ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐻 𝑦 ) )
12 11 rexbidva ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐶 ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ ∃ 𝑥 ∈ 𝐶 𝑥 𝐻 𝑦 ) )
13 3 12 bitr4id ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐻 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
14 fvex ⊢ ( 𝐻 ‘ 𝐷 ) ∈ V
15 2 eliniseg ⊢ ( ( 𝐻 ‘ 𝐷 ) ∈ V → ( 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
16 14 15 mp1i ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
17 13 16 anbi12d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝑦 ∈ ( 𝐻 “ 𝐶 ) ∧ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( ∃ 𝑥 ∈ 𝐶 ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
18 elin ⊢ ( 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( 𝑦 ∈ ( 𝐻 “ 𝐶 ) ∧ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
19 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝐶 ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ↔ ( ∃ 𝑥 ∈ 𝐶 ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
20 17 18 19 3bitr4g ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ∃ 𝑥 ∈ 𝐶 ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
21 20 adantrr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ∃ 𝑥 ∈ 𝐶 ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
22 breq1 ⊢ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ↔ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
23 22 biimpar ⊢ ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) )
24 vex ⊢ 𝑥 ∈ V
25 24 eliniseg ⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ 𝑥 𝑅 𝐷 ) )
26 25 ad2antll ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ 𝑥 𝑅 𝐷 ) )
27 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
28 26 27 bitrd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
29 23 28 imbitrrid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
30 29 exp32 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐷 ∈ 𝐴 → ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) ) ) )
31 4 30 syl9r ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → ( 𝐷 ∈ 𝐴 → ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) ) ) ) )
32 31 com34 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 → ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) ) ) ) )
33 32 imp32 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) ) )
34 33 reximdvai ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∃ 𝑥 ∈ 𝐶 ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐶 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
35 21 34 sylbid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) → ∃ 𝑥 ∈ 𝐶 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
36 elin ⊢ ( 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
37 36 exbii ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
38 neq0 ⊢ ( ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) )
39 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐶 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
40 37 38 39 3bitr4i ⊢ ( ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐶 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) )
41 35 40 imbitrrdi ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) → ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ) )
42 41 exlimdv ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∃ 𝑦 𝑦 ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) → ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ) )
43 1 42 biimtrid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ → ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ) )
44 43 con4d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ → ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
45 5 6 syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 Fn 𝐴 )
46 fnfvima ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) )
47 46 3expia ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝐶 → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
48 47 adantrr ⊢ ( ( 𝐻 Fn 𝐴 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
49 45 48 sylan ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
50 49 adantrd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ) )
51 27 biimpd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝐷 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
52 fvex ⊢ ( 𝐻 ‘ 𝑥 ) ∈ V
53 52 eliniseg ⊢ ( ( 𝐻 ‘ 𝐷 ) ∈ V → ( ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
54 14 53 ax-mp ⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) )
55 51 54 imbitrrdi ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝐷 → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
56 26 55 sylbid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
57 56 exp32 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) ) )
58 4 57 syl9r ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝑥 ∈ 𝐶 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) ) ) )
59 58 com34 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) ) ) )
60 59 imp32 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) )
61 60 impd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
62 50 61 jcad ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ∧ ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) )
63 elin ⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( ( 𝐻 ‘ 𝑥 ) ∈ ( 𝐻 “ 𝐶 ) ∧ ( 𝐻 ‘ 𝑥 ) ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
64 62 36 63 3imtr4g ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ) )
65 n0i ⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ )
66 64 65 syl6 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
67 66 exlimdv ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
68 38 67 biimtrid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ → ¬ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )
69 44 68 impcon4bid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐶 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) = ∅ ↔ ( ( 𝐻 “ 𝐶 ) ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = ∅ ) )