Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfmgc2lem Structured version   Visualization version   GIF version

Theorem dfmgc2lem 30747
 Description: Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
Hypotheses
Ref Expression
mgcoval.1 𝐴 = (Base‘𝑉)
mgcoval.2 𝐵 = (Base‘𝑊)
mgcoval.3 = (le‘𝑉)
mgcoval.4 = (le‘𝑊)
mgcval.1 𝐻 = (𝑉MGalConn𝑊)
mgcval.2 (𝜑𝑉 ∈ Proset )
mgcval.3 (𝜑𝑊 ∈ Proset )
dfmgc2lem.1 (𝜑𝐹:𝐴𝐵)
dfmgc2lem.2 (𝜑𝐺:𝐵𝐴)
dfmgc2lem.3 (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
dfmgc2lem.4 (𝜑 → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
dfmgc2lem.5 ((𝜑𝑥𝐴) → 𝑥 (𝐺‘(𝐹𝑥)))
dfmgc2lem.6 ((𝜑𝑢𝐵) → (𝐹‘(𝐺𝑢)) 𝑢)
Assertion
Ref Expression
dfmgc2lem (𝜑𝐹𝐻𝐺)
Distinct variable groups:   𝑣,   𝑣,   𝑣,𝐴,𝑥,𝑦   𝑣,𝐵,𝑥,𝑦   𝑣,𝑉,𝑥,𝑦   𝑣,𝑊,𝑥,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑢, ,𝑣   𝑥, ,𝑦   𝑢,   𝑥, ,𝑦   𝑢,𝐴   𝑢,𝐵   𝑢,𝐹,𝑣   𝑢,𝐺,𝑣   𝜑,𝑢   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑣)   𝐻(𝑥,𝑦,𝑣,𝑢)   𝑉(𝑢)   𝑊(𝑢)

Proof of Theorem dfmgc2lem
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfmgc2lem.1 . . 3 (𝜑𝐹:𝐴𝐵)
2 dfmgc2lem.2 . . 3 (𝜑𝐺:𝐵𝐴)
31, 2jca 515 . 2 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐵𝐴))
4 mgcval.2 . . . . . . 7 (𝜑𝑉 ∈ Proset )
54ad3antrrr 729 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑉 ∈ Proset )
6 simplr 768 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → 𝑧𝐴)
76adantr 484 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑧𝐴)
82ad3antrrr 729 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝐺:𝐵𝐴)
91ad3antrrr 729 . . . . . . . 8 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝐹:𝐴𝐵)
109, 7ffvelrnd 6839 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐹𝑧) ∈ 𝐵)
118, 10ffvelrnd 6839 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐺‘(𝐹𝑧)) ∈ 𝐴)
122ad2antrr 725 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → 𝐺:𝐵𝐴)
13 simpr 488 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → 𝑤𝐵)
1412, 13ffvelrnd 6839 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (𝐺𝑤) ∈ 𝐴)
1514adantr 484 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐺𝑤) ∈ 𝐴)
16 dfmgc2lem.5 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝑥 (𝐺‘(𝐹𝑥)))
1716ralrimiva 3149 . . . . . . . 8 (𝜑 → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
1817ad3antrrr 729 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
19 simpr 488 . . . . . . . . 9 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
2019fveq2d 6659 . . . . . . . . . 10 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → (𝐹𝑥) = (𝐹𝑧))
2120fveq2d 6659 . . . . . . . . 9 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹𝑥)) = (𝐺‘(𝐹𝑧)))
2219, 21breq12d 5047 . . . . . . . 8 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 (𝐺‘(𝐹𝑥)) ↔ 𝑧 (𝐺‘(𝐹𝑧))))
237, 22rspcdv 3564 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)) → 𝑧 (𝐺‘(𝐹𝑧))))
2418, 23mpd 15 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑧 (𝐺‘(𝐹𝑧)))
25 dfmgc2lem.4 . . . . . . . . 9 (𝜑 → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
2625ad2antrr 725 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
27 breq1 5037 . . . . . . . . . 10 (𝑢 = (𝐹𝑧) → (𝑢 𝑣 ↔ (𝐹𝑧) 𝑣))
28 fveq2 6655 . . . . . . . . . . 11 (𝑢 = (𝐹𝑧) → (𝐺𝑢) = (𝐺‘(𝐹𝑧)))
2928breq1d 5044 . . . . . . . . . 10 (𝑢 = (𝐹𝑧) → ((𝐺𝑢) (𝐺𝑣) ↔ (𝐺‘(𝐹𝑧)) (𝐺𝑣)))
3027, 29imbi12d 348 . . . . . . . . 9 (𝑢 = (𝐹𝑧) → ((𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) ↔ ((𝐹𝑧) 𝑣 → (𝐺‘(𝐹𝑧)) (𝐺𝑣))))
31 breq2 5038 . . . . . . . . . 10 (𝑣 = 𝑤 → ((𝐹𝑧) 𝑣 ↔ (𝐹𝑧) 𝑤))
32 fveq2 6655 . . . . . . . . . . 11 (𝑣 = 𝑤 → (𝐺𝑣) = (𝐺𝑤))
3332breq2d 5046 . . . . . . . . . 10 (𝑣 = 𝑤 → ((𝐺‘(𝐹𝑧)) (𝐺𝑣) ↔ (𝐺‘(𝐹𝑧)) (𝐺𝑤)))
3431, 33imbi12d 348 . . . . . . . . 9 (𝑣 = 𝑤 → (((𝐹𝑧) 𝑣 → (𝐺‘(𝐹𝑧)) (𝐺𝑣)) ↔ ((𝐹𝑧) 𝑤 → (𝐺‘(𝐹𝑧)) (𝐺𝑤))))
351ffvelrnda 6838 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
3635adantr 484 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (𝐹𝑧) ∈ 𝐵)
37 eqidd 2799 . . . . . . . . 9 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑢 = (𝐹𝑧)) → 𝐵 = 𝐵)
3830, 34, 36, 37, 13rspc2vd 3879 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) → ((𝐹𝑧) 𝑤 → (𝐺‘(𝐹𝑧)) (𝐺𝑤))))
3926, 38mpd 15 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ((𝐹𝑧) 𝑤 → (𝐺‘(𝐹𝑧)) (𝐺𝑤)))
4039imp 410 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐺‘(𝐹𝑧)) (𝐺𝑤))
41 mgcoval.1 . . . . . . 7 𝐴 = (Base‘𝑉)
42 mgcoval.3 . . . . . . 7 = (le‘𝑉)
4341, 42prstr 17555 . . . . . 6 ((𝑉 ∈ Proset ∧ (𝑧𝐴 ∧ (𝐺‘(𝐹𝑧)) ∈ 𝐴 ∧ (𝐺𝑤) ∈ 𝐴) ∧ (𝑧 (𝐺‘(𝐹𝑧)) ∧ (𝐺‘(𝐹𝑧)) (𝐺𝑤))) → 𝑧 (𝐺𝑤))
445, 7, 11, 15, 24, 40, 43syl132anc 1385 . . . . 5 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑧 (𝐺𝑤))
45 mgcval.3 . . . . . . 7 (𝜑𝑊 ∈ Proset )
4645ad3antrrr 729 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → 𝑊 ∈ Proset )
4735ad2antrr 725 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹𝑧) ∈ 𝐵)
481ad3antrrr 729 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → 𝐹:𝐴𝐵)
4914adantr 484 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐺𝑤) ∈ 𝐴)
5048, 49ffvelrnd 6839 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹‘(𝐺𝑤)) ∈ 𝐵)
51 simplr 768 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → 𝑤𝐵)
52 dfmgc2lem.3 . . . . . . . . 9 (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
5352ad2antrr 725 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
54 breq1 5037 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 𝑦𝑧 𝑦))
55 fveq2 6655 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
5655breq1d 5044 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝐹𝑥) (𝐹𝑦) ↔ (𝐹𝑧) (𝐹𝑦)))
5754, 56imbi12d 348 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ↔ (𝑧 𝑦 → (𝐹𝑧) (𝐹𝑦))))
58 breq2 5038 . . . . . . . . . 10 (𝑦 = (𝐺𝑤) → (𝑧 𝑦𝑧 (𝐺𝑤)))
59 fveq2 6655 . . . . . . . . . . 11 (𝑦 = (𝐺𝑤) → (𝐹𝑦) = (𝐹‘(𝐺𝑤)))
6059breq2d 5046 . . . . . . . . . 10 (𝑦 = (𝐺𝑤) → ((𝐹𝑧) (𝐹𝑦) ↔ (𝐹𝑧) (𝐹‘(𝐺𝑤))))
6158, 60imbi12d 348 . . . . . . . . 9 (𝑦 = (𝐺𝑤) → ((𝑧 𝑦 → (𝐹𝑧) (𝐹𝑦)) ↔ (𝑧 (𝐺𝑤) → (𝐹𝑧) (𝐹‘(𝐺𝑤)))))
62 eqidd 2799 . . . . . . . . 9 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
6357, 61, 6, 62, 14rspc2vd 3879 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) → (𝑧 (𝐺𝑤) → (𝐹𝑧) (𝐹‘(𝐺𝑤)))))
6453, 63mpd 15 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (𝑧 (𝐺𝑤) → (𝐹𝑧) (𝐹‘(𝐺𝑤))))
6564imp 410 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹𝑧) (𝐹‘(𝐺𝑤)))
66 dfmgc2lem.6 . . . . . . . . 9 ((𝜑𝑢𝐵) → (𝐹‘(𝐺𝑢)) 𝑢)
6766ralrimiva 3149 . . . . . . . 8 (𝜑 → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
6867ad3antrrr 729 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
69 simpr 488 . . . . . . . . . . 11 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
7069fveq2d 6659 . . . . . . . . . 10 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → (𝐺𝑢) = (𝐺𝑤))
7170fveq2d 6659 . . . . . . . . 9 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝑤)))
7271, 69breq12d 5047 . . . . . . . 8 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺𝑢)) 𝑢 ↔ (𝐹‘(𝐺𝑤)) 𝑤))
7351, 72rspcdv 3564 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 → (𝐹‘(𝐺𝑤)) 𝑤))
7468, 73mpd 15 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹‘(𝐺𝑤)) 𝑤)
75 mgcoval.2 . . . . . . 7 𝐵 = (Base‘𝑊)
76 mgcoval.4 . . . . . . 7 = (le‘𝑊)
7775, 76prstr 17555 . . . . . 6 ((𝑊 ∈ Proset ∧ ((𝐹𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺𝑤)) ∈ 𝐵𝑤𝐵) ∧ ((𝐹𝑧) (𝐹‘(𝐺𝑤)) ∧ (𝐹‘(𝐺𝑤)) 𝑤)) → (𝐹𝑧) 𝑤)
7846, 47, 50, 51, 65, 74, 77syl132anc 1385 . . . . 5 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹𝑧) 𝑤)
7944, 78impbida 800 . . . 4 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))
8079anasss 470 . . 3 ((𝜑 ∧ (𝑧𝐴𝑤𝐵)) → ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))
8180ralrimivva 3156 . 2 (𝜑 → ∀𝑧𝐴𝑤𝐵 ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))
82 mgcval.1 . . 3 𝐻 = (𝑉MGalConn𝑊)
8341, 75, 42, 76, 82, 4, 45mgcval 30739 . 2 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ∀𝑧𝐴𝑤𝐵 ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))))
843, 81, 83mpbir2and 712 1 (𝜑𝐹𝐻𝐺)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106   class class class wbr 5034  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145  Basecbs 16495  lecple 16584   Proset cproset 17548  MGalConncmgc 30731 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8409  df-proset 17550  df-mgc 30733 This theorem is referenced by:  dfmgc2  30748
 Copyright terms: Public domain W3C validator