Metamath Proof Explorer


Theorem mnuprdlem1

Description: Lemma for mnuprd . (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypotheses mnuprdlem1.1 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
mnuprdlem1.3 ( 𝜑𝐴𝑈 )
mnuprdlem1.4 ( 𝜑𝐵𝑈 )
mnuprdlem1.8 ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) )
Assertion mnuprdlem1 ( 𝜑𝐴𝑤 )

Proof

Step Hyp Ref Expression
1 mnuprdlem1.1 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
2 mnuprdlem1.3 ( 𝜑𝐴𝑈 )
3 mnuprdlem1.4 ( 𝜑𝐵𝑈 )
4 mnuprdlem1.8 ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) )
5 eleq1 ( 𝑖 = ∅ → ( 𝑖𝑢 ↔ ∅ ∈ 𝑢 ) )
6 5 anbi1d ( 𝑖 = ∅ → ( ( 𝑖𝑢 𝑢𝑤 ) ↔ ( ∅ ∈ 𝑢 𝑢𝑤 ) ) )
7 6 rexbidv ( 𝑖 = ∅ → ( ∃ 𝑢𝐹 ( 𝑖𝑢 𝑢𝑤 ) ↔ ∃ 𝑢𝐹 ( ∅ ∈ 𝑢 𝑢𝑤 ) ) )
8 0ex ∅ ∈ V
9 8 prid1 ∅ ∈ { ∅ , { ∅ } }
10 9 a1i ( 𝜑 → ∅ ∈ { ∅ , { ∅ } } )
11 7 4 10 rspcdva ( 𝜑 → ∃ 𝑢𝐹 ( ∅ ∈ 𝑢 𝑢𝑤 ) )
12 2 adantr ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝐴𝑈 )
13 simprl ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝑎𝐹 )
14 simpr ( ( 𝜑 ∧ ∅ ∈ 𝑎 ) → ∅ ∈ 𝑎 )
15 0nep0 ∅ ≠ { ∅ }
16 15 a1i ( 𝜑 → ∅ ≠ { ∅ } )
17 3 snn0d ( 𝜑 → { 𝐵 } ≠ ∅ )
18 17 necomd ( 𝜑 → ∅ ≠ { 𝐵 } )
19 16 18 nelprd ( 𝜑 → ¬ ∅ ∈ { { ∅ } , { 𝐵 } } )
20 19 adantr ( ( 𝜑 ∧ ∅ ∈ 𝑎 ) → ¬ ∅ ∈ { { ∅ } , { 𝐵 } } )
21 14 20 elnelneqd ( ( 𝜑 ∧ ∅ ∈ 𝑎 ) → ¬ 𝑎 = { { ∅ } , { 𝐵 } } )
22 21 adantrr ( ( 𝜑 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) → ¬ 𝑎 = { { ∅ } , { 𝐵 } } )
23 22 adantrl ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → ¬ 𝑎 = { { ∅ } , { 𝐵 } } )
24 elpri ( 𝑎 ∈ { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } } → ( 𝑎 = { ∅ , { 𝐴 } } ∨ 𝑎 = { { ∅ } , { 𝐵 } } ) )
25 24 1 eleq2s ( 𝑎𝐹 → ( 𝑎 = { ∅ , { 𝐴 } } ∨ 𝑎 = { { ∅ } , { 𝐵 } } ) )
26 25 orcomd ( 𝑎𝐹 → ( 𝑎 = { { ∅ } , { 𝐵 } } ∨ 𝑎 = { ∅ , { 𝐴 } } ) )
27 26 ord ( 𝑎𝐹 → ( ¬ 𝑎 = { { ∅ } , { 𝐵 } } → 𝑎 = { ∅ , { 𝐴 } } ) )
28 13 23 27 sylc ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝑎 = { ∅ , { 𝐴 } } )
29 28 unieqd ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝑎 = { ∅ , { 𝐴 } } )
30 snex { 𝐴 } ∈ V
31 8 30 unipr { ∅ , { 𝐴 } } = ( ∅ ∪ { 𝐴 } )
32 uncom ( ∅ ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ∅ )
33 un0 ( { 𝐴 } ∪ ∅ ) = { 𝐴 }
34 31 32 33 3eqtri { ∅ , { 𝐴 } } = { 𝐴 }
35 29 34 eqtrdi ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝑎 = { 𝐴 } )
36 simprrr ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝑎𝑤 )
37 35 36 eqsstrrd ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → { 𝐴 } ⊆ 𝑤 )
38 snssg ( 𝐴𝑈 → ( 𝐴𝑤 ↔ { 𝐴 } ⊆ 𝑤 ) )
39 38 biimprd ( 𝐴𝑈 → ( { 𝐴 } ⊆ 𝑤𝐴𝑤 ) )
40 12 37 39 sylc ( ( 𝜑 ∧ ( 𝑎𝐹 ∧ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) ) → 𝐴𝑤 )
41 eleq2w ( 𝑢 = 𝑎 → ( ∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎 ) )
42 unieq ( 𝑢 = 𝑎 𝑢 = 𝑎 )
43 42 sseq1d ( 𝑢 = 𝑎 → ( 𝑢𝑤 𝑎𝑤 ) )
44 41 43 anbi12d ( 𝑢 = 𝑎 → ( ( ∅ ∈ 𝑢 𝑢𝑤 ) ↔ ( ∅ ∈ 𝑎 𝑎𝑤 ) ) )
45 11 40 44 rexlimddvcbvw ( 𝜑𝐴𝑤 )