Metamath Proof Explorer

Theorem supisoex

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

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

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢ ( 𝜑 → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 supiso.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 supisoex.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) )
4 simpl ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
5 simpr ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ⊆ 𝐴 )
6 4 5 supisolem ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
7 isof1o ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
8 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 4 7 8 3syl ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
10 9 ffvelrnda ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11 breq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( 𝑢 𝑆 𝑤 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ) )
12 11 notbid ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( ¬ 𝑢 𝑆 𝑤 ↔ ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ) )
13 12 ralbidv ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ↔ ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ) )
14 breq2 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( 𝑤 𝑆 𝑢 ↔ 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
15 14 imbi1d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ↔ ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
16 15 ralbidv ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
17 13 16 anbi12d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑥 ) → ( ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
18 17 rspcev ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
19 18 ex ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 → ( ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
20 10 19 syl ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ 𝑥 ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ 𝑥 ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
21 6 20 sylbid ⊢ ( ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
22 21 rexlimdva ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
23 1 2 22 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
24 3 23 mpd ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐵 ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ 𝑢 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 𝑢 → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )