Theorem mnuprdlem2

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

	Ref	Expression
Hypotheses	mnuprdlem2.1	⊢ 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
	mnuprdlem2.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
	mnuprdlem2.5	⊢ ( 𝜑 → ¬ 𝐴 = ∅ )
	mnuprdlem2.8	⊢ ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
Assertion	mnuprdlem2	⊢ ( 𝜑 → 𝐵 ∈ 𝑤 )

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem2.1	⊢ 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
2		mnuprdlem2.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
3		mnuprdlem2.5	⊢ ( 𝜑 → ¬ 𝐴 = ∅ )
4		mnuprdlem2.8	⊢ ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
5		eleq1	⊢ ( 𝑖 = { ∅ } → ( 𝑖 ∈ 𝑢 ↔ { ∅ } ∈ 𝑢 ) )
6	5	anbi1d	⊢ ( 𝑖 = { ∅ } → ( ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( { ∅ } ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
7	6	rexbidv	⊢ ( 𝑖 = { ∅ } → ( ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝐹 ( { ∅ } ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
8		p0ex	⊢ { ∅ } ∈ V
9	8	prid2	⊢ { ∅ } ∈ { ∅ , { ∅ } }
10	9	a1i	⊢ ( 𝜑 → { ∅ } ∈ { ∅ , { ∅ } } )
11	7 4 10	rspcdva	⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐹 ( { ∅ } ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
12		simpl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝜑 )
13		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝑎 ∈ 𝐹 )
14		simpr	⊢ ( ( 𝜑 ∧ { ∅ } ∈ 𝑎 ) → { ∅ } ∈ 𝑎 )
15		0nep0	⊢ ∅ ≠ { ∅ }
16	15	necomi	⊢ { ∅ } ≠ ∅
17	16	a1i	⊢ ( 𝜑 → { ∅ } ≠ ∅ )
18		0ex	⊢ ∅ ∈ V
19	18	sneqr	⊢ ( { ∅ } = { 𝐴 } → ∅ = 𝐴 )
20	19	eqcomd	⊢ ( { ∅ } = { 𝐴 } → 𝐴 = ∅ )
21	3 20	nsyl	⊢ ( 𝜑 → ¬ { ∅ } = { 𝐴 } )
22	21	neqned	⊢ ( 𝜑 → { ∅ } ≠ { 𝐴 } )
23	17 22	nelprd	⊢ ( 𝜑 → ¬ { ∅ } ∈ { ∅ , { 𝐴 } } )
24	23	adantr	⊢ ( ( 𝜑 ∧ { ∅ } ∈ 𝑎 ) → ¬ { ∅ } ∈ { ∅ , { 𝐴 } } )
25	14 24	elnelneqd	⊢ ( ( 𝜑 ∧ { ∅ } ∈ 𝑎 ) → ¬ 𝑎 = { ∅ , { 𝐴 } } )
26	25	adantrr	⊢ ( ( 𝜑 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) → ¬ 𝑎 = { ∅ , { 𝐴 } } )
27	26	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ¬ 𝑎 = { ∅ , { 𝐴 } } )
28		elpri	⊢ ( 𝑎 ∈ { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } } → ( 𝑎 = { ∅ , { 𝐴 } } ∨ 𝑎 = { { ∅ } , { 𝐵 } } ) )
29	28 1	eleq2s	⊢ ( 𝑎 ∈ 𝐹 → ( 𝑎 = { ∅ , { 𝐴 } } ∨ 𝑎 = { { ∅ } , { 𝐵 } } ) )
30	29	ord	⊢ ( 𝑎 ∈ 𝐹 → ( ¬ 𝑎 = { ∅ , { 𝐴 } } → 𝑎 = { { ∅ } , { 𝐵 } } ) )
31	13 27 30	sylc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝑎 = { { ∅ } , { 𝐵 } } )
32	31	unieqd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ∪ 𝑎 = ∪ { { ∅ } , { 𝐵 } } )
33		snex	⊢ { 𝐵 } ∈ V
34	8 33	unipr	⊢ ∪ { { ∅ } , { 𝐵 } } = ( { ∅ } ∪ { 𝐵 } )
35		df-pr	⊢ { ∅ , 𝐵 } = ( { ∅ } ∪ { 𝐵 } )
36	34 35	eqtr4i	⊢ ∪ { { ∅ } , { 𝐵 } } = { ∅ , 𝐵 }
37	32 36	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ∪ 𝑎 = { ∅ , 𝐵 } )
38		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ∪ 𝑎 ⊆ 𝑤 )
39	37 38	eqsstrrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → { ∅ , 𝐵 } ⊆ 𝑤 )
40		prssg	⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑈 ) → ( ( ∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤 ) ↔ { ∅ , 𝐵 } ⊆ 𝑤 ) )
41	18 2 40	sylancr	⊢ ( 𝜑 → ( ( ∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤 ) ↔ { ∅ , 𝐵 } ⊆ 𝑤 ) )
42	41	biimprd	⊢ ( 𝜑 → ( { ∅ , 𝐵 } ⊆ 𝑤 → ( ∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤 ) ) )
43	12 39 42	sylc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → ( ∅ ∈ 𝑤 ∧ 𝐵 ∈ 𝑤 ) )
44	43	simprd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐹 ∧ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) ) → 𝐵 ∈ 𝑤 )
45		eleq2w	⊢ ( 𝑢 = 𝑎 → ( { ∅ } ∈ 𝑢 ↔ { ∅ } ∈ 𝑎 ) )
46		unieq	⊢ ( 𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎 )
47	46	sseq1d	⊢ ( 𝑢 = 𝑎 → ( ∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤 ) )
48	45 47	anbi12d	⊢ ( 𝑢 = 𝑎 → ( ( { ∅ } ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( { ∅ } ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤 ) ) )
49	11 44 48	rexlimddvcbvw	⊢ ( 𝜑 → 𝐵 ∈ 𝑤 )