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	⊢ ( 𝜑 → 𝐴 ∈ 𝑤 )