Users' Mathboxes Mathbox for Rohan Ridenour < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  grumnudlem Structured version   Visualization version   GIF version

Theorem grumnudlem 43346
Description: Lemma for grumnud 43347. (Contributed by Rohan Ridenour, 13-Aug-2023.)
Hypotheses
Ref Expression
grumnudlem.1 𝑀 = {π‘˜ ∣ βˆ€π‘™ ∈ π‘˜ (𝒫 𝑙 βŠ† π‘˜ ∧ βˆ€π‘šβˆƒπ‘› ∈ π‘˜ (𝒫 𝑙 βŠ† 𝑛 ∧ βˆ€π‘ ∈ 𝑙 (βˆƒπ‘ž ∈ π‘˜ (𝑝 ∈ π‘ž ∧ π‘ž ∈ π‘š) β†’ βˆƒπ‘Ÿ ∈ π‘š (𝑝 ∈ π‘Ÿ ∧ βˆͺ π‘Ÿ βŠ† 𝑛))))}
grumnudlem.2 (πœ‘ β†’ 𝐺 ∈ Univ)
grumnudlem.3 𝐹 = ({βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘(βˆͺ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 Γ— 𝐺))
grumnudlem.4 ((𝑖 ∈ 𝐺 ∧ β„Ž ∈ 𝐺) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
grumnudlem.5 ((β„Ž ∈ (𝐹 Coll 𝑧) ∧ (βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
Assertion
Ref Expression
grumnudlem (πœ‘ β†’ 𝐺 ∈ 𝑀)
Distinct variable groups:   πœ‘,𝑧,𝑓,β„Ž,𝑗   𝑧,𝐺   𝑓,β„Ž,𝑗,𝐺   πœ‘,𝑓,β„Ž,𝑖,𝑗   𝑒,β„Ž,𝑖,𝑗,𝐹   𝑧,𝑖,π‘˜,π‘š,𝑛,π‘ž,𝑝,𝑙,𝑓,𝐺   𝑧,𝑒,π‘Ÿ,𝑓,π‘˜,π‘š,𝑛,𝐺,𝑝,𝑙,𝑖
Allowed substitution hints:   πœ‘(𝑒,π‘˜,π‘š,𝑛,π‘Ÿ,π‘ž,𝑝,𝑏,𝑐,𝑑,𝑙)   𝐹(𝑧,𝑓,π‘˜,π‘š,𝑛,π‘Ÿ,π‘ž,𝑝,𝑏,𝑐,𝑑,𝑙)   𝐺(𝑏,𝑐,𝑑)   𝑀(𝑧,𝑒,𝑓,β„Ž,𝑖,𝑗,π‘˜,π‘š,𝑛,π‘Ÿ,π‘ž,𝑝,𝑏,𝑐,𝑑,𝑙)

Proof of Theorem grumnudlem
Dummy variables π‘Ž 𝑀 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grumnudlem.2 . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ Univ)
2 gruss 10793 . . . . . . . 8 ((𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ∧ π‘Ž βŠ† 𝑧) β†’ π‘Ž ∈ 𝐺)
31, 2syl3an1 1161 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ π‘Ž βŠ† 𝑧) β†’ π‘Ž ∈ 𝐺)
433expia 1119 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (π‘Ž βŠ† 𝑧 β†’ π‘Ž ∈ 𝐺))
54alrimiv 1928 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆ€π‘Ž(π‘Ž βŠ† 𝑧 β†’ π‘Ž ∈ 𝐺))
6 pwss 4624 . . . . 5 (𝒫 𝑧 βŠ† 𝐺 ↔ βˆ€π‘Ž(π‘Ž βŠ† 𝑧 β†’ π‘Ž ∈ 𝐺))
75, 6sylibr 233 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝒫 𝑧 βŠ† 𝐺)
8 ssun1 4171 . . . . . . . . 9 𝒫 𝑧 βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))
9 simp3 1136 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
108, 9sseqtrrid 4034 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ 𝒫 𝑧 βŠ† 𝑀)
11 simp1l3 1266 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
12 simp1r 1196 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑖 ∈ 𝑧)
13 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ 𝑗 = 𝑣)
1413unieqd 4921 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ βˆͺ 𝑗 = βˆͺ 𝑣)
15 simpl 481 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ β„Ž = βˆͺ 𝑣)
1614, 15eqtr4d 2773 . . . . . . . . . . . . . . . . . . . 20 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ βˆͺ 𝑗 = β„Ž)
1716adantll 710 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ βˆͺ 𝑗 = β„Ž)
18 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑗 = 𝑣)
19 simpll3 1212 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
2019simprd 494 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑣 ∈ 𝑓)
2118, 20eqeltrd 2831 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑗 ∈ 𝑓)
2219simpld 493 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑖 ∈ 𝑣)
2322, 18eleqtrrd 2834 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑖 ∈ 𝑗)
2417, 21, 233jca 1126 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ (βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
25 simpl2 1190 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) β†’ 𝑣 ∈ 𝐺)
2624, 25rr-spce 43258 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) β†’ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
27 simp1l1 1264 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ πœ‘)
2827, 1syl 17 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝐺 ∈ Univ)
29 simp2 1135 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑣 ∈ 𝐺)
30 gruuni 10797 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Univ ∧ 𝑣 ∈ 𝐺) β†’ βˆͺ 𝑣 ∈ 𝐺)
3128, 29, 30syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆͺ 𝑣 ∈ 𝐺)
3226, 31rspcime 3615 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ 𝐺 βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
33 simpl1 1189 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ πœ‘)
3433, 1syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝐺 ∈ Univ)
35 simpl2 1190 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝑧 ∈ 𝐺)
36 simpr 483 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝑖 ∈ 𝑧)
37 gruel 10800 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ∧ 𝑖 ∈ 𝑧) β†’ 𝑖 ∈ 𝐺)
3834, 35, 36, 37syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝑖 ∈ 𝐺)
39383ad2ant1 1131 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑖 ∈ 𝐺)
40 grumnudlem.4 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ 𝐺 ∧ β„Ž ∈ 𝐺) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
4139, 40sylan 578 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ 𝐺) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
4241rexbidva 3174 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ (βˆƒβ„Ž ∈ 𝐺 π‘–πΉβ„Ž ↔ βˆƒβ„Ž ∈ 𝐺 βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
4332, 42mpbird 256 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ 𝐺 π‘–πΉβ„Ž)
44 rexex 3074 . . . . . . . . . . . . . . 15 (βˆƒβ„Ž ∈ 𝐺 π‘–πΉβ„Ž β†’ βˆƒβ„Ž π‘–πΉβ„Ž)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž π‘–πΉβ„Ž)
4612, 45cpcoll2d 43320 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)π‘–πΉβ„Ž)
4728adantr 479 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ 𝐺 ∈ Univ)
48353ad2ant1 1131 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑧 ∈ 𝐺)
4948adantr 479 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ 𝑧 ∈ 𝐺)
501adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝐺 ∈ Univ)
51 grumnudlem.3 . . . . . . . . . . . . . . . . . . . 20 𝐹 = ({βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘(βˆͺ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 Γ— 𝐺))
52 inss2 4228 . . . . . . . . . . . . . . . . . . . 20 ({βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘(βˆͺ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 Γ— 𝐺)) βŠ† (𝐺 Γ— 𝐺)
5351, 52eqsstri 4015 . . . . . . . . . . . . . . . . . . 19 𝐹 βŠ† (𝐺 Γ— 𝐺)
5453a1i 11 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝐹 βŠ† (𝐺 Γ— 𝐺))
55 simpr 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝑧 ∈ 𝐺)
5650, 54, 55grucollcld 43321 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (𝐹 Coll 𝑧) ∈ 𝐺)
5727, 49, 56syl2an2r 681 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ (𝐹 Coll 𝑧) ∈ 𝐺)
58 simpr 483 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ β„Ž ∈ (𝐹 Coll 𝑧))
59 gruel 10800 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Univ ∧ (𝐹 Coll 𝑧) ∈ 𝐺 ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ β„Ž ∈ 𝐺)
6047, 57, 58, 59syl3anc 1369 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ β„Ž ∈ 𝐺)
6139, 60, 40syl2an2r 681 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
6261rexbidva 3174 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)π‘–πΉβ„Ž ↔ βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
6346, 62mpbid 231 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
64 rexcom4 3283 . . . . . . . . . . . . 13 (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) ↔ βˆƒπ‘—βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
65 grumnudlem.5 . . . . . . . . . . . . . . 15 ((β„Ž ∈ (𝐹 Coll 𝑧) ∧ (βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6665rexlimiva 3145 . . . . . . . . . . . . . 14 (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6766exlimiv 1931 . . . . . . . . . . . . 13 (βˆƒπ‘—βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6864, 67sylbi 216 . . . . . . . . . . . 12 (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6963, 68syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
70 elssuni 4940 . . . . . . . . . . . . . . . . 17 (βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧) β†’ βˆͺ 𝑒 βŠ† βˆͺ (𝐹 Coll 𝑧))
71 ssun2 4172 . . . . . . . . . . . . . . . . 17 βˆͺ (𝐹 Coll 𝑧) βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))
7270, 71sstrdi 3993 . . . . . . . . . . . . . . . 16 (βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧) β†’ βˆͺ 𝑒 βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
7372adantl 480 . . . . . . . . . . . . . . 15 ((𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ βˆͺ 𝑒 βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
74 simpl 481 . . . . . . . . . . . . . . 15 ((𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
7573, 74sseqtrrd 4022 . . . . . . . . . . . . . 14 ((𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ βˆͺ 𝑒 βŠ† 𝑀)
7675ex 411 . . . . . . . . . . . . 13 (𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) β†’ (βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧) β†’ βˆͺ 𝑒 βŠ† 𝑀))
7776anim2d 610 . . . . . . . . . . . 12 (𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) β†’ ((𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
7877reximdv 3168 . . . . . . . . . . 11 (𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) β†’ (βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
7911, 69, 78sylc 65 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))
8079rexlimdv3a 3157 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
8180ralrimiva 3144 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
8210, 81jca 510 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
83823expa 1116 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ 𝐺) ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
84 grupw 10792 . . . . . . . 8 ((𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺) β†’ 𝒫 𝑧 ∈ 𝐺)
851, 84sylan 578 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝒫 𝑧 ∈ 𝐺)
86 gruuni 10797 . . . . . . . 8 ((𝐺 ∈ Univ ∧ (𝐹 Coll 𝑧) ∈ 𝐺) β†’ βˆͺ (𝐹 Coll 𝑧) ∈ 𝐺)
871, 56, 86syl2an2r 681 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆͺ (𝐹 Coll 𝑧) ∈ 𝐺)
88 gruun 10803 . . . . . . 7 ((𝐺 ∈ Univ ∧ 𝒫 𝑧 ∈ 𝐺 ∧ βˆͺ (𝐹 Coll 𝑧) ∈ 𝐺) β†’ (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∈ 𝐺)
8950, 85, 87, 88syl3anc 1369 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∈ 𝐺)
9083, 89rspcime 3615 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
9190alrimiv 1928 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
927, 91jca 510 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))))
9392ralrimiva 3144 . 2 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))))
94 grumnudlem.1 . . . 4 𝑀 = {π‘˜ ∣ βˆ€π‘™ ∈ π‘˜ (𝒫 𝑙 βŠ† π‘˜ ∧ βˆ€π‘šβˆƒπ‘› ∈ π‘˜ (𝒫 𝑙 βŠ† 𝑛 ∧ βˆ€π‘ ∈ 𝑙 (βˆƒπ‘ž ∈ π‘˜ (𝑝 ∈ π‘ž ∧ π‘ž ∈ π‘š) β†’ βˆƒπ‘Ÿ ∈ π‘š (𝑝 ∈ π‘Ÿ ∧ βˆͺ π‘Ÿ βŠ† 𝑛))))}
9594ismnu 43322 . . 3 (𝐺 ∈ Univ β†’ (𝐺 ∈ 𝑀 ↔ βˆ€π‘§ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))))
961, 95syl 17 . 2 (πœ‘ β†’ (𝐺 ∈ 𝑀 ↔ βˆ€π‘§ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))))
9793, 96mpbird 256 1 (πœ‘ β†’ 𝐺 ∈ 𝑀)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104  {cab 2707  βˆ€wral 3059  βˆƒwrex 3068   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601  βˆͺ cuni 4907   class class class wbr 5147  {copab 5209   Γ— cxp 5673  Univcgru 10787   Coll ccoll 43311
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-reg 9589  ax-inf2 9638  ax-ac2 10460
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-tc 9734  df-r1 9761  df-rank 9762  df-card 9936  df-cf 9938  df-acn 9939  df-ac 10113  df-wina 10681  df-ina 10682  df-gru 10788  df-scott 43297  df-coll 43312
This theorem is referenced by:  grumnud  43347
  Copyright terms: Public domain W3C validator