Metamath Proof Explorer

Theorem grpoidinvlem3

Description: Lemma for grpoidinv . (Contributed by NM, 11-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpfo.1 ⊢X=ran⁡G
grpidinvlem3.2 ⊢φ↔∀x∈XUGx=x
grpidinvlem3.3 ⊢ψ↔∀x∈X∃z∈XzGx=U
Assertion grpoidinvlem3 ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X→∃y∈XyGA=U∧AGy=U

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢X=ran⁡G
2 grpidinvlem3.2 ⊢φ↔∀x∈XUGx=x
3 grpidinvlem3.3 ⊢ψ↔∀x∈X∃z∈XzGx=U
4 oveq1 ⊢z=y→zGx=yGx
5 4 eqeq1d ⊢z=y→zGx=U↔yGx=U
6 5 cbvrexvw ⊢∃z∈XzGx=U↔∃y∈XyGx=U
7 6 ralbii ⊢∀x∈X∃z∈XzGx=U↔∀x∈X∃y∈XyGx=U
8 3 7 bitri ⊢ψ↔∀x∈X∃y∈XyGx=U
9 oveq2 ⊢x=A→yGx=yGA
10 9 eqeq1d ⊢x=A→yGx=U↔yGA=U
11 10 rexbidv ⊢x=A→∃y∈XyGx=U↔∃y∈XyGA=U
12 11 rspccva ⊢∀x∈X∃y∈XyGx=U∧A∈X→∃y∈XyGA=U
13 8 12 sylanb ⊢ψ∧A∈X→∃y∈XyGA=U
14 13 adantll ⊢φ∧ψ∧A∈X→∃y∈XyGA=U
15 14 adantll ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X→∃y∈XyGA=U
16 1 grpocl ⊢G∈GrpOp∧A∈X∧y∈X→AGy∈X
17 16 3expa ⊢G∈GrpOp∧A∈X∧y∈X→AGy∈X
18 17 adantllr ⊢G∈GrpOp∧U∈X∧A∈X∧y∈X→AGy∈X
19 18 adantllr ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→AGy∈X
20 2 biimpi ⊢φ→∀x∈XUGx=x
21 20 ad2antrl ⊢G∈GrpOp∧U∈X∧φ∧ψ→∀x∈XUGx=x
22 21 ad2antrr ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→∀x∈XUGx=x
23 oveq2 ⊢x=AGy→UGx=UGAGy
24 id ⊢x=AGy→x=AGy
25 23 24 eqeq12d ⊢x=AGy→UGx=x↔UGAGy=AGy
26 25 rspcva ⊢AGy∈X∧∀x∈XUGx=x→UGAGy=AGy
27 19 22 26 syl2anc ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→UGAGy=AGy
28 27 adantr ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→UGAGy=AGy
29 pm3.22 ⊢y∈X∧A∈X∧G∈GrpOp→G∈GrpOp∧y∈X∧A∈X
30 29 an31s ⊢G∈GrpOp∧A∈X∧y∈X→G∈GrpOp∧y∈X∧A∈X
31 30 adantllr ⊢G∈GrpOp∧U∈X∧A∈X∧y∈X→G∈GrpOp∧y∈X∧A∈X
32 31 adantllr ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→G∈GrpOp∧y∈X∧A∈X
33 32 adantr ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→G∈GrpOp∧y∈X∧A∈X
34 oveq2 ⊢x=y→UGx=UGy
35 id ⊢x=y→x=y
36 34 35 eqeq12d ⊢x=y→UGx=x↔UGy=y
37 36 rspccva ⊢∀x∈XUGx=x∧y∈X→UGy=y
38 2 37 sylanb ⊢φ∧y∈X→UGy=y
39 38 adantlr ⊢φ∧ψ∧y∈X→UGy=y
40 39 adantlr ⊢φ∧ψ∧A∈X∧y∈X→UGy=y
41 40 adantlll ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→UGy=y
42 41 anim1i ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→UGy=y∧yGA=U
43 1 grpoidinvlem2 ⊢G∈GrpOp∧y∈X∧A∈X∧UGy=y∧yGA=U→AGyGAGy=AGy
44 33 42 43 syl2anc ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→AGyGAGy=AGy
45 16 3expb ⊢G∈GrpOp∧A∈X∧y∈X→AGy∈X
46 45 ad2ant2rl ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X→AGy∈X
47 oveq1 ⊢z=w→zGx=wGx
48 47 eqeq1d ⊢z=w→zGx=U↔wGx=U
49 48 cbvrexvw ⊢∃z∈XzGx=U↔∃w∈XwGx=U
50 49 ralbii ⊢∀x∈X∃z∈XzGx=U↔∀x∈X∃w∈XwGx=U
51 3 50 bitri ⊢ψ↔∀x∈X∃w∈XwGx=U
52 oveq2 ⊢x=AGy→wGx=wGAGy
53 52 eqeq1d ⊢x=AGy→wGx=U↔wGAGy=U
54 53 rexbidv ⊢x=AGy→∃w∈XwGx=U↔∃w∈XwGAGy=U
55 54 rspcva ⊢AGy∈X∧∀x∈X∃w∈XwGx=U→∃w∈XwGAGy=U
56 51 55 sylan2b ⊢AGy∈X∧ψ→∃w∈XwGAGy=U
57 anass ⊢G∈GrpOp∧w∈X∧AGy∈X↔G∈GrpOp∧w∈X∧AGy∈X
58 57 biimpi ⊢G∈GrpOp∧w∈X∧AGy∈X→G∈GrpOp∧w∈X∧AGy∈X
59 58 an32s ⊢G∈GrpOp∧AGy∈X∧w∈X→G∈GrpOp∧w∈X∧AGy∈X
60 59 ex ⊢G∈GrpOp∧AGy∈X→w∈X→G∈GrpOp∧w∈X∧AGy∈X
61 45 60 syldan ⊢G∈GrpOp∧A∈X∧y∈X→w∈X→G∈GrpOp∧w∈X∧AGy∈X
62 61 ad2ant2rl ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X→w∈X→G∈GrpOp∧w∈X∧AGy∈X
63 62 imp ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X∧w∈X→G∈GrpOp∧w∈X∧AGy∈X
64 1 grpoidinvlem1 ⊢G∈GrpOp∧w∈X∧AGy∈X∧wGAGy=U∧AGyGAGy=AGy→UGAGy=U
65 63 64 sylan ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X∧w∈X∧wGAGy=U∧AGyGAGy=AGy→UGAGy=U
66 65 exp43 ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X→w∈X→wGAGy=U→AGyGAGy=AGy→UGAGy=U
67 66 rexlimdv ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X→∃w∈XwGAGy=U→AGyGAGy=AGy→UGAGy=U
68 56 67 syl5 ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X→AGy∈X∧ψ→AGyGAGy=AGy→UGAGy=U
69 46 68 mpand ⊢G∈GrpOp∧U∈X∧φ∧A∈X∧y∈X→ψ→AGyGAGy=AGy→UGAGy=U
70 69 exp32 ⊢G∈GrpOp∧U∈X→φ→A∈X∧y∈X→ψ→AGyGAGy=AGy→UGAGy=U
71 70 com34 ⊢G∈GrpOp∧U∈X→φ→ψ→A∈X∧y∈X→AGyGAGy=AGy→UGAGy=U
72 71 imp32 ⊢G∈GrpOp∧U∈X∧φ∧ψ→A∈X∧y∈X→AGyGAGy=AGy→UGAGy=U
73 72 impl ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→AGyGAGy=AGy→UGAGy=U
74 73 adantr ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→AGyGAGy=AGy→UGAGy=U
75 44 74 mpd ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→UGAGy=U
76 28 75 eqtr3d ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X∧yGA=U→AGy=U
77 76 ex ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→yGA=U→AGy=U
78 77 ancld ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X∧y∈X→yGA=U→yGA=U∧AGy=U
79 78 reximdva ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X→∃y∈XyGA=U→∃y∈XyGA=U∧AGy=U
80 15 79 mpd ⊢G∈GrpOp∧U∈X∧φ∧ψ∧A∈X→∃y∈XyGA=U∧AGy=U