Metamath Proof Explorer

Theorem grumnudlem

Description: Lemma for grumnud . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses grumnudlem.1 ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
grumnudlem.2 ⊢ ( 𝜑 → 𝐺 ∈ Univ )
grumnudlem.3 ⊢ 𝐹 = ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) )
grumnudlem.4 ⊢ ( ( 𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺 ) → ( 𝑖 𝐹 ℎ ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
grumnudlem.5 ⊢ ( ( ℎ ∈ ( 𝐹 Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) )
Assertion grumnudlem ( 𝜑 → 𝐺 ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 grumnudlem.1 ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2 grumnudlem.2 ⊢ ( 𝜑 → 𝐺 ∈ Univ )
3 grumnudlem.3 ⊢ 𝐹 = ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) )
4 grumnudlem.4 ⊢ ( ( 𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺 ) → ( 𝑖 𝐹 ℎ ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
5 grumnudlem.5 ⊢ ( ( ℎ ∈ ( 𝐹 Coll 𝑧 ) ∧ ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) )
6 gruss ⊢ ( ( 𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ∧ 𝑎 ⊆ 𝑧 ) → 𝑎 ∈ 𝐺 )
7 2 6 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑎 ⊆ 𝑧 ) → 𝑎 ∈ 𝐺 )
8 7 3expia ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ( 𝑎 ⊆ 𝑧 → 𝑎 ∈ 𝐺 ) )
9 8 alrimiv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ∀ 𝑎 ( 𝑎 ⊆ 𝑧 → 𝑎 ∈ 𝐺 ) )
10 pwss ⊢ ( 𝒫 𝑧 ⊆ 𝐺 ↔ ∀ 𝑎 ( 𝑎 ⊆ 𝑧 → 𝑎 ∈ 𝐺 ) )
11 9 10 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → 𝒫 𝑧 ⊆ 𝐺 )
12 ssun1 ⊢ 𝒫 𝑧 ⊆ ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) )
13 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) → 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) )
14 12 13 sseqtrrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) → 𝒫 𝑧 ⊆ 𝑤 )
15 simp1l3 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) )
16 simp1r ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑖 ∈ 𝑧 )
17 simpr ⊢ ( ( ℎ = ∪ 𝑣 ∧ 𝑗 = 𝑣 ) → 𝑗 = 𝑣 )
18 17 unieqd ⊢ ( ( ℎ = ∪ 𝑣 ∧ 𝑗 = 𝑣 ) → ∪ 𝑗 = ∪ 𝑣 )
19 simpl ⊢ ( ( ℎ = ∪ 𝑣 ∧ 𝑗 = 𝑣 ) → ℎ = ∪ 𝑣 )
20 18 19 eqtr4d ⊢ ( ( ℎ = ∪ 𝑣 ∧ 𝑗 = 𝑣 ) → ∪ 𝑗 = ℎ )
21 20 adantll ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → ∪ 𝑗 = ℎ )
22 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → 𝑗 = 𝑣 )
23 simpll3 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
24 23 simprd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → 𝑣 ∈ 𝑓 )
25 22 24 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → 𝑗 ∈ 𝑓 )
26 23 simpld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → 𝑖 ∈ 𝑣 )
27 26 22 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → 𝑖 ∈ 𝑗 )
28 21 25 27 3jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) ∧ 𝑗 = 𝑣 ) → ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) )
29 simpl2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) → 𝑣 ∈ 𝐺 )
30 28 29 rr-spce ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ = ∪ 𝑣 ) → ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) )
31 simp1l1 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝜑 )
32 31 2 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝐺 ∈ Univ )
33 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑣 ∈ 𝐺 )
34 gruuni ⊢ ( ( 𝐺 ∈ Univ ∧ 𝑣 ∈ 𝐺 ) → ∪ 𝑣 ∈ 𝐺 )
35 32 33 34 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∪ 𝑣 ∈ 𝐺 )
36 30 35 rspcime ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ ℎ ∈ 𝐺 ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) )
37 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) → 𝜑 )
38 37 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) → 𝐺 ∈ Univ )
39 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) → 𝑧 ∈ 𝐺 )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) → 𝑖 ∈ 𝑧 )
41 gruel ⊢ ( ( 𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ∧ 𝑖 ∈ 𝑧 ) → 𝑖 ∈ 𝐺 )
42 38 39 40 41 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) → 𝑖 ∈ 𝐺 )
43 42 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑖 ∈ 𝐺 )
44 43 4 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ 𝐺 ) → ( 𝑖 𝐹 ℎ ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
45 44 rexbidva ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ( ∃ ℎ ∈ 𝐺 𝑖 𝐹 ℎ ↔ ∃ ℎ ∈ 𝐺 ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
46 36 45 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ ℎ ∈ 𝐺 𝑖 𝐹 ℎ )
47 rexex ⊢ ( ∃ ℎ ∈ 𝐺 𝑖 𝐹 ℎ → ∃ ℎ 𝑖 𝐹 ℎ )
48 46 47 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ ℎ 𝑖 𝐹 ℎ )
49 16 48 cpcoll2d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) 𝑖 𝐹 ℎ )
50 32 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → 𝐺 ∈ Univ )
51 39 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑧 ∈ 𝐺 )
52 51 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → 𝑧 ∈ 𝐺 )
53 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → 𝐺 ∈ Univ )
54 inss2 ⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ( ∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑 ) } ∩ ( 𝐺 × 𝐺 ) ) ⊆ ( 𝐺 × 𝐺 )
55 3 54 eqsstri ⊢ 𝐹 ⊆ ( 𝐺 × 𝐺 )
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → 𝐹 ⊆ ( 𝐺 × 𝐺 ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → 𝑧 ∈ 𝐺 )
58 53 56 57 grucollcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ( 𝐹 Coll 𝑧 ) ∈ 𝐺 )
59 31 52 58 syl2an2r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → ( 𝐹 Coll 𝑧 ) ∈ 𝐺 )
60 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → ℎ ∈ ( 𝐹 Coll 𝑧 ) )
61 gruel ⊢ ( ( 𝐺 ∈ Univ ∧ ( 𝐹 Coll 𝑧 ) ∈ 𝐺 ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → ℎ ∈ 𝐺 )
62 50 59 60 61 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → ℎ ∈ 𝐺 )
63 43 62 4 syl2an2r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) ∧ ℎ ∈ ( 𝐹 Coll 𝑧 ) ) → ( 𝑖 𝐹 ℎ ↔ ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
64 63 rexbidva ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ( ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) 𝑖 𝐹 ℎ ↔ ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ) )
65 49 64 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) )
66 rexcom4 ⊢ ( ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) ↔ ∃ 𝑗 ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) )
67 5 rexlimiva ⊢ ( ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) )
68 67 exlimiv ⊢ ( ∃ 𝑗 ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) )
69 66 68 sylbi ⊢ ( ∃ ℎ ∈ ( 𝐹 Coll 𝑧 ) ∃ 𝑗 ( ∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) )
70 65 69 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) )
71 elssuni ⊢ ( ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) → ∪ 𝑢 ⊆ ∪ ( 𝐹 Coll 𝑧 ) )
72 ssun2 ⊢ ∪ ( 𝐹 Coll 𝑧 ) ⊆ ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) )
73 71 72 sstrdi ⊢ ( ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) → ∪ 𝑢 ⊆ ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) )
74 73 adantl ⊢ ( ( 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) → ∪ 𝑢 ⊆ ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) )
75 simpl ⊢ ( ( 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) → 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) )
76 74 75 sseqtrrd ⊢ ( ( 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) → ∪ 𝑢 ⊆ 𝑤 )
77 76 ex ⊢ ( 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) → ( ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) → ∪ 𝑢 ⊆ 𝑤 ) )
78 77 anim2d ⊢ ( 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) → ( ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) → ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
79 78 reximdv ⊢ ( 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) → ( ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ ( 𝐹 Coll 𝑧 ) ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
80 15 70 79 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) ∧ 𝑣 ∈ 𝐺 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
81 80 rexlimdv3a ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) ∧ 𝑖 ∈ 𝑧 ) → ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
82 81 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) → ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
83 14 82 jca ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) → ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
84 83 3expa ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) ∧ 𝑤 = ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ) → ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
85 grupw ⊢ ( ( 𝐺 ∈ Univ ∧ 𝑧 ∈ 𝐺 ) → 𝒫 𝑧 ∈ 𝐺 )
86 2 85 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → 𝒫 𝑧 ∈ 𝐺 )
87 gruuni ⊢ ( ( 𝐺 ∈ Univ ∧ ( 𝐹 Coll 𝑧 ) ∈ 𝐺 ) → ∪ ( 𝐹 Coll 𝑧 ) ∈ 𝐺 )
88 2 58 87 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ∪ ( 𝐹 Coll 𝑧 ) ∈ 𝐺 )
89 gruun ⊢ ( ( 𝐺 ∈ Univ ∧ 𝒫 𝑧 ∈ 𝐺 ∧ ∪ ( 𝐹 Coll 𝑧 ) ∈ 𝐺 ) → ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ∈ 𝐺 )
90 53 86 88 89 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ( 𝒫 𝑧 ∪ ∪ ( 𝐹 Coll 𝑧 ) ) ∈ 𝐺 )
91 84 90 rspcime ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ∃ 𝑤 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
92 91 alrimiv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ∀ 𝑓 ∃ 𝑤 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
93 11 92 jca ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) → ( 𝒫 𝑧 ⊆ 𝐺 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
94 93 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝐺 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
95 1 ismnu ⊢ ( 𝐺 ∈ Univ → ( 𝐺 ∈ 𝑀 ↔ ∀ 𝑧 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝐺 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) )
96 2 95 syl ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑀 ↔ ∀ 𝑧 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝐺 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝐺 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝐺 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) )
97 94 96 mpbird ⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )