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 43044
Description: Lemma for grumnud 43045. (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 10791 . . . . . . . 8 ((𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ∧ π‘Ž βŠ† 𝑧) β†’ π‘Ž ∈ 𝐺)
31, 2syl3an1 1164 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ π‘Ž βŠ† 𝑧) β†’ π‘Ž ∈ 𝐺)
433expia 1122 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (π‘Ž βŠ† 𝑧 β†’ π‘Ž ∈ 𝐺))
54alrimiv 1931 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆ€π‘Ž(π‘Ž βŠ† 𝑧 β†’ π‘Ž ∈ 𝐺))
6 pwss 4626 . . . . 5 (𝒫 𝑧 βŠ† 𝐺 ↔ βˆ€π‘Ž(π‘Ž βŠ† 𝑧 β†’ π‘Ž ∈ 𝐺))
75, 6sylibr 233 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝒫 𝑧 βŠ† 𝐺)
8 ssun1 4173 . . . . . . . . 9 𝒫 𝑧 βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))
9 simp3 1139 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
108, 9sseqtrrid 4036 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ 𝒫 𝑧 βŠ† 𝑀)
11 simp1l3 1269 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
12 simp1r 1199 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑖 ∈ 𝑧)
13 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ 𝑗 = 𝑣)
1413unieqd 4923 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ βˆͺ 𝑗 = βˆͺ 𝑣)
15 simpl 484 . . . . . . . . . . . . . . . . . . . . 21 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ β„Ž = βˆͺ 𝑣)
1614, 15eqtr4d 2776 . . . . . . . . . . . . . . . . . . . 20 ((β„Ž = βˆͺ 𝑣 ∧ 𝑗 = 𝑣) β†’ βˆͺ 𝑗 = β„Ž)
1716adantll 713 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ βˆͺ 𝑗 = β„Ž)
18 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑗 = 𝑣)
19 simpll3 1215 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
2019simprd 497 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑣 ∈ 𝑓)
2118, 20eqeltrd 2834 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑗 ∈ 𝑓)
2219simpld 496 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑖 ∈ 𝑣)
2322, 18eleqtrrd 2837 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ 𝑖 ∈ 𝑗)
2417, 21, 233jca 1129 . . . . . . . . . . . . . . . . . 18 ((((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) ∧ 𝑗 = 𝑣) β†’ (βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
25 simpl2 1193 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) β†’ 𝑣 ∈ 𝐺)
2624, 25rr-spce 42956 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž = βˆͺ 𝑣) β†’ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
27 simp1l1 1267 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ πœ‘)
2827, 1syl 17 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝐺 ∈ Univ)
29 simp2 1138 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑣 ∈ 𝐺)
30 gruuni 10795 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Univ ∧ 𝑣 ∈ 𝐺) β†’ βˆͺ 𝑣 ∈ 𝐺)
3128, 29, 30syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆͺ 𝑣 ∈ 𝐺)
3226, 31rspcime 3617 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ 𝐺 βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
33 simpl1 1192 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ πœ‘)
3433, 1syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝐺 ∈ Univ)
35 simpl2 1193 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝑧 ∈ 𝐺)
36 simpr 486 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝑖 ∈ 𝑧)
37 gruel 10798 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ∧ 𝑖 ∈ 𝑧) β†’ 𝑖 ∈ 𝐺)
3834, 35, 36, 37syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ 𝑖 ∈ 𝐺)
39383ad2ant1 1134 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑖 ∈ 𝐺)
40 grumnudlem.4 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ 𝐺 ∧ β„Ž ∈ 𝐺) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
4139, 40sylan 581 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ 𝐺) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
4241rexbidva 3177 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ (βˆƒβ„Ž ∈ 𝐺 π‘–πΉβ„Ž ↔ βˆƒβ„Ž ∈ 𝐺 βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
4332, 42mpbird 257 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ 𝐺 π‘–πΉβ„Ž)
44 rexex 3077 . . . . . . . . . . . . . . 15 (βˆƒβ„Ž ∈ 𝐺 π‘–πΉβ„Ž β†’ βˆƒβ„Ž π‘–πΉβ„Ž)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž π‘–πΉβ„Ž)
4612, 45cpcoll2d 43018 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)π‘–πΉβ„Ž)
4728adantr 482 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ 𝐺 ∈ Univ)
48353ad2ant1 1134 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ 𝑧 ∈ 𝐺)
4948adantr 482 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ 𝑧 ∈ 𝐺)
501adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝐺 ∈ Univ)
51 grumnudlem.3 . . . . . . . . . . . . . . . . . . . 20 𝐹 = ({βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘(βˆͺ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 Γ— 𝐺))
52 inss2 4230 . . . . . . . . . . . . . . . . . . . 20 ({βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘(βˆͺ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 Γ— 𝐺)) βŠ† (𝐺 Γ— 𝐺)
5351, 52eqsstri 4017 . . . . . . . . . . . . . . . . . . 19 𝐹 βŠ† (𝐺 Γ— 𝐺)
5453a1i 11 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝐹 βŠ† (𝐺 Γ— 𝐺))
55 simpr 486 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝑧 ∈ 𝐺)
5650, 54, 55grucollcld 43019 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (𝐹 Coll 𝑧) ∈ 𝐺)
5727, 49, 56syl2an2r 684 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ (𝐹 Coll 𝑧) ∈ 𝐺)
58 simpr 486 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ β„Ž ∈ (𝐹 Coll 𝑧))
59 gruel 10798 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Univ ∧ (𝐹 Coll 𝑧) ∈ 𝐺 ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ β„Ž ∈ 𝐺)
6047, 57, 58, 59syl3anc 1372 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ β„Ž ∈ 𝐺)
6139, 60, 40syl2an2r 684 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) ∧ β„Ž ∈ (𝐹 Coll 𝑧)) β†’ (π‘–πΉβ„Ž ↔ βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
6261rexbidva 3177 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)π‘–πΉβ„Ž ↔ βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)))
6346, 62mpbid 231 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
64 rexcom4 3286 . . . . . . . . . . . . 13 (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) ↔ βˆƒπ‘—βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))
65 grumnudlem.5 . . . . . . . . . . . . . . 15 ((β„Ž ∈ (𝐹 Coll 𝑧) ∧ (βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6665rexlimiva 3148 . . . . . . . . . . . . . 14 (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6766exlimiv 1934 . . . . . . . . . . . . 13 (βˆƒπ‘—βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6864, 67sylbi 216 . . . . . . . . . . . 12 (βˆƒβ„Ž ∈ (𝐹 Coll 𝑧)βˆƒπ‘—(βˆͺ 𝑗 = β„Ž ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
6963, 68syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)))
70 elssuni 4942 . . . . . . . . . . . . . . . . 17 (βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧) β†’ βˆͺ 𝑒 βŠ† βˆͺ (𝐹 Coll 𝑧))
71 ssun2 4174 . . . . . . . . . . . . . . . . 17 βˆͺ (𝐹 Coll 𝑧) βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))
7270, 71sstrdi 3995 . . . . . . . . . . . . . . . 16 (βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧) β†’ βˆͺ 𝑒 βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
7372adantl 483 . . . . . . . . . . . . . . 15 ((𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ βˆͺ 𝑒 βŠ† (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
74 simpl 484 . . . . . . . . . . . . . . 15 ((𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)))
7573, 74sseqtrrd 4024 . . . . . . . . . . . . . 14 ((𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ βˆͺ 𝑒 βŠ† 𝑀)
7675ex 414 . . . . . . . . . . . . 13 (𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) β†’ (βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧) β†’ βˆͺ 𝑒 βŠ† 𝑀))
7776anim2d 613 . . . . . . . . . . . 12 (𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) β†’ ((𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
7877reximdv 3171 . . . . . . . . . . 11 (𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) β†’ (βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 ∈ (𝐹 Coll 𝑧)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
7911, 69, 78sylc 65 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) ∧ 𝑣 ∈ 𝐺 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))
8079rexlimdv3a 3160 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) ∧ 𝑖 ∈ 𝑧) β†’ (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
8180ralrimiva 3147 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))
8210, 81jca 513 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺 ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
83823expa 1119 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ 𝐺) ∧ 𝑀 = (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧))) β†’ (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
84 grupw 10790 . . . . . . . 8 ((𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺) β†’ 𝒫 𝑧 ∈ 𝐺)
851, 84sylan 581 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ 𝒫 𝑧 ∈ 𝐺)
86 gruuni 10795 . . . . . . . 8 ((𝐺 ∈ Univ ∧ (𝐹 Coll 𝑧) ∈ 𝐺) β†’ βˆͺ (𝐹 Coll 𝑧) ∈ 𝐺)
871, 56, 86syl2an2r 684 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆͺ (𝐹 Coll 𝑧) ∈ 𝐺)
88 gruun 10801 . . . . . . 7 ((𝐺 ∈ Univ ∧ 𝒫 𝑧 ∈ 𝐺 ∧ βˆͺ (𝐹 Coll 𝑧) ∈ 𝐺) β†’ (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∈ 𝐺)
8950, 85, 87, 88syl3anc 1372 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (𝒫 𝑧 βˆͺ βˆͺ (𝐹 Coll 𝑧)) ∈ 𝐺)
9083, 89rspcime 3617 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
9190alrimiv 1931 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))
927, 91jca 513 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝐺) β†’ (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))))
9392ralrimiva 3147 . 2 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀)))))
94 grumnudlem.1 . . . 4 𝑀 = {π‘˜ ∣ βˆ€π‘™ ∈ π‘˜ (𝒫 𝑙 βŠ† π‘˜ ∧ βˆ€π‘šβˆƒπ‘› ∈ π‘˜ (𝒫 𝑙 βŠ† 𝑛 ∧ βˆ€π‘ ∈ 𝑙 (βˆƒπ‘ž ∈ π‘˜ (𝑝 ∈ π‘ž ∧ π‘ž ∈ π‘š) β†’ βˆƒπ‘Ÿ ∈ π‘š (𝑝 ∈ π‘Ÿ ∧ βˆͺ π‘Ÿ βŠ† 𝑛))))}
9594ismnu 43020 . . 3 (𝐺 ∈ Univ β†’ (𝐺 ∈ 𝑀 ↔ βˆ€π‘§ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))))
961, 95syl 17 . 2 (πœ‘ β†’ (𝐺 ∈ 𝑀 ↔ βˆ€π‘§ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝐺 ∧ βˆ€π‘“βˆƒπ‘€ ∈ 𝐺 (𝒫 𝑧 βŠ† 𝑀 ∧ βˆ€π‘– ∈ 𝑧 (βˆƒπ‘£ ∈ 𝐺 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) β†’ βˆƒπ‘’ ∈ 𝑓 (𝑖 ∈ 𝑒 ∧ βˆͺ 𝑒 βŠ† 𝑀))))))
9793, 96mpbird 257 1 (πœ‘ β†’ 𝐺 ∈ 𝑀)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  βˆƒwrex 3071   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  βˆͺ cuni 4909   class class class wbr 5149  {copab 5211   Γ— cxp 5675  Univcgru 10785   Coll ccoll 43009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-reg 9587  ax-inf2 9636  ax-ac2 10458
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-tc 9732  df-r1 9759  df-rank 9760  df-card 9934  df-cf 9936  df-acn 9937  df-ac 10111  df-wina 10679  df-ina 10680  df-gru 10786  df-scott 42995  df-coll 43010
This theorem is referenced by:  grumnud  43045
  Copyright terms: Public domain W3C validator