Metamath Proof Explorer


Theorem mnuop23d

Description: Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuop23d.1 𝑀 = { 𝑘 ∣ ∀ 𝑙𝑘 ( 𝒫 𝑙𝑘 ∧ ∀ 𝑚𝑛𝑘 ( 𝒫 𝑙𝑛 ∧ ∀ 𝑝𝑙 ( ∃ 𝑞𝑘 ( 𝑝𝑞𝑞𝑚 ) → ∃ 𝑟𝑚 ( 𝑝𝑟 𝑟𝑛 ) ) ) ) }
mnuop23d.2 ( 𝜑𝑈𝑀 )
mnuop23d.3 ( 𝜑𝐴𝑈 )
mnuop23d.4 ( 𝜑𝐹𝑉 )
Assertion mnuop23d ( 𝜑 → ∃ 𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 mnuop23d.1 𝑀 = { 𝑘 ∣ ∀ 𝑙𝑘 ( 𝒫 𝑙𝑘 ∧ ∀ 𝑚𝑛𝑘 ( 𝒫 𝑙𝑛 ∧ ∀ 𝑝𝑙 ( ∃ 𝑞𝑘 ( 𝑝𝑞𝑞𝑚 ) → ∃ 𝑟𝑚 ( 𝑝𝑟 𝑟𝑛 ) ) ) ) }
2 mnuop23d.2 ( 𝜑𝑈𝑀 )
3 mnuop23d.3 ( 𝜑𝐴𝑈 )
4 mnuop23d.4 ( 𝜑𝐹𝑉 )
5 1 2 3 mnuop123d ( 𝜑 → ( 𝒫 𝐴𝑈 ∧ ∀ 𝑓𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
6 5 simprd ( 𝜑 → ∀ 𝑓𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) )
7 eleq2 ( 𝑓 = 𝐹 → ( 𝑣𝑓𝑣𝐹 ) )
8 7 anbi2d ( 𝑓 = 𝐹 → ( ( 𝑖𝑣𝑣𝑓 ) ↔ ( 𝑖𝑣𝑣𝐹 ) ) )
9 8 rexbidv ( 𝑓 = 𝐹 → ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) ↔ ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) ) )
10 rexeq ( 𝑓 = 𝐹 → ( ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ↔ ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) )
11 9 10 imbi12d ( 𝑓 = 𝐹 → ( ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) )
12 11 ralbidv ( 𝑓 = 𝐹 → ( ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) )
13 12 anbi2d ( 𝑓 = 𝐹 → ( ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
14 13 rexbidv ( 𝑓 = 𝐹 → ( ∃ 𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ∃ 𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
15 14 spcgv ( 𝐹𝑉 → ( ∀ 𝑓𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) → ∃ 𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
16 4 6 15 sylc ( 𝜑 → ∃ 𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝐹 ) → ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ) ) )