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

Theorem dfmgc2lem 32985
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 511 . 2 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐵𝐴))
4 mgcval.2 . . . . . . 7 (𝜑𝑉 ∈ Proset )
54ad3antrrr 730 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑉 ∈ Proset )
6 simplr 769 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → 𝑧𝐴)
76adantr 480 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑧𝐴)
82ad3antrrr 730 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝐺:𝐵𝐴)
91ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝐹:𝐴𝐵)
109, 7ffvelcdmd 7105 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐹𝑧) ∈ 𝐵)
118, 10ffvelcdmd 7105 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐺‘(𝐹𝑧)) ∈ 𝐴)
122ad2antrr 726 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → 𝐺:𝐵𝐴)
13 simpr 484 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → 𝑤𝐵)
1412, 13ffvelcdmd 7105 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (𝐺𝑤) ∈ 𝐴)
1514adantr 480 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐺𝑤) ∈ 𝐴)
16 dfmgc2lem.5 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝑥 (𝐺‘(𝐹𝑥)))
1716ralrimiva 3146 . . . . . . . 8 (𝜑 → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
1817ad3antrrr 730 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))
19 simpr 484 . . . . . . . . 9 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧)
2019fveq2d 6910 . . . . . . . . . 10 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → (𝐹𝑥) = (𝐹𝑧))
2120fveq2d 6910 . . . . . . . . 9 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → (𝐺‘(𝐹𝑥)) = (𝐺‘(𝐹𝑧)))
2219, 21breq12d 5156 . . . . . . . 8 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) ∧ 𝑥 = 𝑧) → (𝑥 (𝐺‘(𝐹𝑥)) ↔ 𝑧 (𝐺‘(𝐹𝑧))))
237, 22rspcdv 3614 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)) → 𝑧 (𝐺‘(𝐹𝑧))))
2418, 23mpd 15 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑧 (𝐺‘(𝐹𝑧)))
25 dfmgc2lem.4 . . . . . . . . 9 (𝜑 → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
2625ad2antrr 726 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))
27 breq1 5146 . . . . . . . . . 10 (𝑢 = (𝐹𝑧) → (𝑢 𝑣 ↔ (𝐹𝑧) 𝑣))
28 fveq2 6906 . . . . . . . . . . 11 (𝑢 = (𝐹𝑧) → (𝐺𝑢) = (𝐺‘(𝐹𝑧)))
2928breq1d 5153 . . . . . . . . . 10 (𝑢 = (𝐹𝑧) → ((𝐺𝑢) (𝐺𝑣) ↔ (𝐺‘(𝐹𝑧)) (𝐺𝑣)))
3027, 29imbi12d 344 . . . . . . . . 9 (𝑢 = (𝐹𝑧) → ((𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) ↔ ((𝐹𝑧) 𝑣 → (𝐺‘(𝐹𝑧)) (𝐺𝑣))))
31 breq2 5147 . . . . . . . . . 10 (𝑣 = 𝑤 → ((𝐹𝑧) 𝑣 ↔ (𝐹𝑧) 𝑤))
32 fveq2 6906 . . . . . . . . . . 11 (𝑣 = 𝑤 → (𝐺𝑣) = (𝐺𝑤))
3332breq2d 5155 . . . . . . . . . 10 (𝑣 = 𝑤 → ((𝐺‘(𝐹𝑧)) (𝐺𝑣) ↔ (𝐺‘(𝐹𝑧)) (𝐺𝑤)))
3431, 33imbi12d 344 . . . . . . . . 9 (𝑣 = 𝑤 → (((𝐹𝑧) 𝑣 → (𝐺‘(𝐹𝑧)) (𝐺𝑣)) ↔ ((𝐹𝑧) 𝑤 → (𝐺‘(𝐹𝑧)) (𝐺𝑤))))
351ffvelcdmda 7104 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
3635adantr 480 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (𝐹𝑧) ∈ 𝐵)
37 eqidd 2738 . . . . . . . . 9 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑢 = (𝐹𝑧)) → 𝐵 = 𝐵)
3830, 34, 36, 37, 13rspc2vd 3947 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)) → ((𝐹𝑧) 𝑤 → (𝐺‘(𝐹𝑧)) (𝐺𝑤))))
3926, 38mpd 15 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ((𝐹𝑧) 𝑤 → (𝐺‘(𝐹𝑧)) (𝐺𝑤)))
4039imp 406 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → (𝐺‘(𝐹𝑧)) (𝐺𝑤))
41 mgcoval.1 . . . . . . 7 𝐴 = (Base‘𝑉)
42 mgcoval.3 . . . . . . 7 = (le‘𝑉)
4341, 42prstr 18345 . . . . . 6 ((𝑉 ∈ Proset ∧ (𝑧𝐴 ∧ (𝐺‘(𝐹𝑧)) ∈ 𝐴 ∧ (𝐺𝑤) ∈ 𝐴) ∧ (𝑧 (𝐺‘(𝐹𝑧)) ∧ (𝐺‘(𝐹𝑧)) (𝐺𝑤))) → 𝑧 (𝐺𝑤))
445, 7, 11, 15, 24, 40, 43syl132anc 1390 . . . . 5 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ (𝐹𝑧) 𝑤) → 𝑧 (𝐺𝑤))
45 mgcval.3 . . . . . . 7 (𝜑𝑊 ∈ Proset )
4645ad3antrrr 730 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → 𝑊 ∈ Proset )
4735ad2antrr 726 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹𝑧) ∈ 𝐵)
481ad3antrrr 730 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → 𝐹:𝐴𝐵)
4914adantr 480 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐺𝑤) ∈ 𝐴)
5048, 49ffvelcdmd 7105 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹‘(𝐺𝑤)) ∈ 𝐵)
51 simplr 769 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → 𝑤𝐵)
52 dfmgc2lem.3 . . . . . . . . 9 (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
5352ad2antrr 726 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))
54 breq1 5146 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 𝑦𝑧 𝑦))
55 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
5655breq1d 5153 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝐹𝑥) (𝐹𝑦) ↔ (𝐹𝑧) (𝐹𝑦)))
5754, 56imbi12d 344 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ↔ (𝑧 𝑦 → (𝐹𝑧) (𝐹𝑦))))
58 breq2 5147 . . . . . . . . . 10 (𝑦 = (𝐺𝑤) → (𝑧 𝑦𝑧 (𝐺𝑤)))
59 fveq2 6906 . . . . . . . . . . 11 (𝑦 = (𝐺𝑤) → (𝐹𝑦) = (𝐹‘(𝐺𝑤)))
6059breq2d 5155 . . . . . . . . . 10 (𝑦 = (𝐺𝑤) → ((𝐹𝑧) (𝐹𝑦) ↔ (𝐹𝑧) (𝐹‘(𝐺𝑤))))
6158, 60imbi12d 344 . . . . . . . . 9 (𝑦 = (𝐺𝑤) → ((𝑧 𝑦 → (𝐹𝑧) (𝐹𝑦)) ↔ (𝑧 (𝐺𝑤) → (𝐹𝑧) (𝐹‘(𝐺𝑤)))))
62 eqidd 2738 . . . . . . . . 9 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑥 = 𝑧) → 𝐴 = 𝐴)
6357, 61, 6, 62, 14rspc2vd 3947 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) → (𝑧 (𝐺𝑤) → (𝐹𝑧) (𝐹‘(𝐺𝑤)))))
6453, 63mpd 15 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → (𝑧 (𝐺𝑤) → (𝐹𝑧) (𝐹‘(𝐺𝑤))))
6564imp 406 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹𝑧) (𝐹‘(𝐺𝑤)))
66 dfmgc2lem.6 . . . . . . . . 9 ((𝜑𝑢𝐵) → (𝐹‘(𝐺𝑢)) 𝑢)
6766ralrimiva 3146 . . . . . . . 8 (𝜑 → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
6867ad3antrrr 730 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → ∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢)
69 simpr 484 . . . . . . . . . . 11 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
7069fveq2d 6910 . . . . . . . . . 10 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → (𝐺𝑢) = (𝐺𝑤))
7170fveq2d 6910 . . . . . . . . 9 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → (𝐹‘(𝐺𝑢)) = (𝐹‘(𝐺𝑤)))
7271, 69breq12d 5156 . . . . . . . 8 (((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) ∧ 𝑢 = 𝑤) → ((𝐹‘(𝐺𝑢)) 𝑢 ↔ (𝐹‘(𝐺𝑤)) 𝑤))
7351, 72rspcdv 3614 . . . . . . 7 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 → (𝐹‘(𝐺𝑤)) 𝑤))
7468, 73mpd 15 . . . . . 6 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹‘(𝐺𝑤)) 𝑤)
75 mgcoval.2 . . . . . . 7 𝐵 = (Base‘𝑊)
76 mgcoval.4 . . . . . . 7 = (le‘𝑊)
7775, 76prstr 18345 . . . . . 6 ((𝑊 ∈ Proset ∧ ((𝐹𝑧) ∈ 𝐵 ∧ (𝐹‘(𝐺𝑤)) ∈ 𝐵𝑤𝐵) ∧ ((𝐹𝑧) (𝐹‘(𝐺𝑤)) ∧ (𝐹‘(𝐺𝑤)) 𝑤)) → (𝐹𝑧) 𝑤)
7846, 47, 50, 51, 65, 74, 77syl132anc 1390 . . . . 5 ((((𝜑𝑧𝐴) ∧ 𝑤𝐵) ∧ 𝑧 (𝐺𝑤)) → (𝐹𝑧) 𝑤)
7944, 78impbida 801 . . . 4 (((𝜑𝑧𝐴) ∧ 𝑤𝐵) → ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))
8079anasss 466 . . 3 ((𝜑 ∧ (𝑧𝐴𝑤𝐵)) → ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))
8180ralrimivva 3202 . 2 (𝜑 → ∀𝑧𝐴𝑤𝐵 ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))
82 mgcval.1 . . 3 𝐻 = (𝑉MGalConn𝑊)
8341, 75, 42, 76, 82, 4, 45mgcval 32977 . 2 (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ∀𝑧𝐴𝑤𝐵 ((𝐹𝑧) 𝑤𝑧 (𝐺𝑤)))))
843, 81, 83mpbir2and 713 1 (𝜑𝐹𝐻𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061   class class class wbr 5143  wf 6557  cfv 6561  (class class class)co 7431  Basecbs 17247  lecple 17304   Proset cproset 18338  MGalConncmgc 32969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-proset 18340  df-mgc 32971
This theorem is referenced by:  dfmgc2  32986
  Copyright terms: Public domain W3C validator