Theorem infisoti 6834

Description: Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.)

Hypotheses

Ref	Expression
infisoti.1	⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))
infisoti.2	⊢ (𝜑 → 𝐶 ⊆ 𝐴)
infisoti.3	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))
infisoti.ti	⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))

Assertion

Ref	Expression
infisoti	⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅)))

Distinct variable groups:   𝑢,𝐴,𝑣,𝑥,𝑦,𝑧   𝑢,𝐵,𝑣,𝑥,𝑦,𝑧   𝑢,𝐶,𝑣,𝑥,𝑦,𝑧   𝑢,𝐹,𝑣,𝑥,𝑦,𝑧   𝑢,𝑅,𝑣,𝑥,𝑦,𝑧   𝑢,𝑆,𝑣,𝑥,𝑦,𝑧   𝜑,𝑢,𝑣,𝑥,𝑦,𝑧

Proof of Theorem infisoti

Step	Hyp	Ref	Expression
1		infisoti.1	. . . 4 ⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))
2		isocnv2 5645	. . . 4 ⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐹 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
3	1, 2	sylib 121	. . 3 ⊢ (𝜑 → 𝐹 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵))
4		infisoti.2	. . 3 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
5		infisoti.3	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))
6	5	cnvinfex 6820	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦◡𝑅𝑧)))
7		infisoti.ti	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))
8	7	cnvti 6821	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢◡𝑅𝑣 ∧ ¬ 𝑣◡𝑅𝑢)))
9	3, 4, 6, 8	supisoti 6812	. 2 ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, ◡𝑆) = (𝐹‘sup(𝐶, 𝐴, ◡𝑅)))
10		df-inf 6787	. 2 ⊢ inf((𝐹 “ 𝐶), 𝐵, 𝑆) = sup((𝐹 “ 𝐶), 𝐵, ◡𝑆)
11		df-inf 6787	. . 3 ⊢ inf(𝐶, 𝐴, 𝑅) = sup(𝐶, 𝐴, ◡𝑅)
12	11	fveq2i 5356	. 2 ⊢ (𝐹‘inf(𝐶, 𝐴, 𝑅)) = (𝐹‘sup(𝐶, 𝐴, ◡𝑅))
13	9, 10, 12	3eqtr4g 2157	1 ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1299   ∈ wcel 1448  ∀wral 2375  ∃wrex 2376   ⊆ wss 3021   class class class wbr 3875  ^◡ccnv 4476   “ cima 4480  ‘cfv 5059   Isom wiso 5060  supcsup 6784  infcinf 6785

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-reu 2382  df-rmo 2383  df-rab 2384  df-v 2643  df-sbc 2863  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-mpt 3931  df-id 4153  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-isom 5068  df-riota 5662  df-sup 6786  df-inf 6787

This theorem is referenced by: (None)