Metamath Proof Explorer

Theorem supisolem

Description: Lemma for supiso . (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supiso.1 ⊢ ( 𝜑 → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
supiso.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion supisolem ( ( 𝜑 ∧ 𝐷 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐷 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐷 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢ ( 𝜑 → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 supiso.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 1 2 jca ⊢ ( 𝜑 → ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) )
4 simpll ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
5 4 adantr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐶 ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
6 simplr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐶 ) → 𝐷 ∈ 𝐴 )
7 simplr ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → 𝐶 ⊆ 𝐴 )
8 7 sselda ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐴 )
9 isorel ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐷 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
10 5 6 8 9 syl12anc ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝐷 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
11 10 notbid ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐶 ) → ( ¬ 𝐷 𝑅 𝑦 ↔ ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
12 11 ralbidva ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐷 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
13 isof1o ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
14 4 13 syl ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
15 f1ofn ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 Fn 𝐴 )
16 14 15 syl ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → 𝐹 Fn 𝐴 )
17 breq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ↔ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
18 17 notbid ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑦 ) → ( ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ↔ ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
19 18 ralima ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ↔ ∀ 𝑦 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
20 16 7 19 syl2anc ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ↔ ∀ 𝑦 ∈ 𝐶 ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
21 12 20 bitr4d ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐷 𝑅 𝑦 ↔ ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ) )
22 4 adantr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
23 simpr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
24 simplr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐷 ∈ 𝐴 )
25 isorel ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
26 22 23 24 25 syl12anc ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝐷 ↔ ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
27 22 adantr ⊢ ( ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐶 ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
28 simplr ⊢ ( ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐶 ) → 𝑦 ∈ 𝐴 )
29 7 adantr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐶 ⊆ 𝐴 )
30 29 sselda ⊢ ( ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ 𝐴 )
31 isorel ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
32 27 28 30 31 syl12anc ⊢ ( ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
33 32 rexbidva ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
34 16 adantr ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐹 Fn 𝐴 )
35 breq2 ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ↔ ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
36 35 rexima ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ↔ ∃ 𝑧 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
37 34 29 36 syl2anc ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ↔ ∃ 𝑧 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
38 33 37 bitr4d ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ↔ ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ) )
39 26 38 imbi12d ⊢ ( ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 𝑅 𝐷 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ) ) )
40 39 ralbidva ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐷 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ) ) )
41 f1ofo ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
42 breq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) ↔ 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) ) )
43 breq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ↔ 𝑤 𝑆 𝑣 ) )
44 43 rexbidv ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ↔ ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) )
45 42 44 imbi12d ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ) ↔ ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
46 45 cbvfo ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
47 14 41 46 3syl ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) ( 𝐹 ‘ 𝑦 ) 𝑆 𝑣 ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
48 40 47 bitrd ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐷 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
49 21 48 anbi12d ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐷 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐷 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
50 3 49 sylan ⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐷 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐷 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝐷 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝐷 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )