Metamath Proof Explorer

Theorem supiso

Description: Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢ ( 𝜑 → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 supiso.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 supisoex.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) )
4 supiso.4 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
5 isoso ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵 ) )
6 1 5 syl ⊢ ( 𝜑 → ( 𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵 ) )
7 4 6 mpbid ⊢ ( 𝜑 → 𝑆 Or 𝐵 )
8 isof1o ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
9 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
10 1 8 9 3syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
11 4 3 supcl ⊢ ( 𝜑 → sup ( 𝐶 , 𝐴 , 𝑅 ) ∈ 𝐴 )
12 10 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) ∈ 𝐵 )
13 4 3 supub ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐶 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑢 ) )
14 13 ralrimiv ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐶 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑢 )
15 4 3 suplub ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 sup ( 𝐶 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐶 𝑢 𝑅 𝑧 ) )
16 15 expd ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐴 → ( 𝑢 𝑅 sup ( 𝐶 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐶 𝑢 𝑅 𝑧 ) ) )
17 16 ralrimiv ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 sup ( 𝐶 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐶 𝑢 𝑅 𝑧 ) )
18 1 2 supisolem ⊢ ( ( 𝜑 ∧ sup ( 𝐶 , 𝐴 , 𝑅 ) ∈ 𝐴 ) → ( ( ∀ 𝑢 ∈ 𝐶 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑢 ∧ ∀ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 sup ( 𝐶 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐶 𝑢 𝑅 𝑧 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
19 11 18 mpdan ⊢ ( 𝜑 → ( ( ∀ 𝑢 ∈ 𝐶 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑢 ∧ ∀ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 sup ( 𝐶 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐶 𝑢 𝑅 𝑧 ) ) ↔ ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) ) )
20 14 17 19 mpbi2and ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) 𝑆 𝑤 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) ) )
21 20 simpld ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ¬ ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) 𝑆 𝑤 )
22 21 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐹 “ 𝐶 ) ) → ¬ ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) 𝑆 𝑤 )
23 20 simprd ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ( 𝑤 𝑆 ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) )
24 23 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 𝑆 ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 ) )
25 24 impr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 𝑆 ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) ) ) → ∃ 𝑣 ∈ ( 𝐹 “ 𝐶 ) 𝑤 𝑆 𝑣 )
26 7 12 22 25 eqsupd ⊢ ( 𝜑 → sup ( ( 𝐹 “ 𝐶 ) , 𝐵 , 𝑆 ) = ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , 𝑅 ) ) )