Theorem fin2solem

Description: Lemma for fin2so . (Contributed by Brendan Leahy, 29-Jun-2019)

	Ref	Expression
Assertion	fin2solem	⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) → ( 𝑦 𝑅 𝑧 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ∧ 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) )
2		3anass	⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) )
3	1 2	bitr4i	⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ∧ 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) )
4		sotr	⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑤 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑤 𝑅 𝑧 ) )
5	3 4	sylan2b	⊢ ( ( 𝑅 Or 𝑥 ∧ ( ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ∧ 𝑤 ∈ 𝑥 ) ) → ( ( 𝑤 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑤 𝑅 𝑧 ) )
6	5	anassrs	⊢ ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑤 ∈ 𝑥 ) → ( ( 𝑤 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑤 𝑅 𝑧 ) )
7	6	ancomsd	⊢ ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑤 ∈ 𝑥 ) → ( ( 𝑦 𝑅 𝑧 ∧ 𝑤 𝑅 𝑦 ) → 𝑤 𝑅 𝑧 ) )
8	7	expdimp	⊢ ( ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑤 ∈ 𝑥 ) ∧ 𝑦 𝑅 𝑧 ) → ( 𝑤 𝑅 𝑦 → 𝑤 𝑅 𝑧 ) )
9	8	an32s	⊢ ( ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑦 𝑅 𝑧 ) ∧ 𝑤 ∈ 𝑥 ) → ( 𝑤 𝑅 𝑦 → 𝑤 𝑅 𝑧 ) )
10	9	ss2rabdv	⊢ ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑦 𝑅 𝑧 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ⊆ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
11		breq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
12	11	elrab	⊢ ( 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 𝑅 𝑧 ) )
13	12	biimpri	⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 𝑅 𝑧 ) → 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
14	13	adantll	⊢ ( ( ( 𝑅 Or 𝑥 ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 𝑅 𝑧 ) → 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
15		sonr	⊢ ( ( 𝑅 Or 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑦 𝑅 𝑦 )
16		breq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑦 ↔ 𝑦 𝑅 𝑦 ) )
17	16	elrab	⊢ ( 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 𝑅 𝑦 ) )
18	17	simprbi	⊢ ( 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } → 𝑦 𝑅 𝑦 )
19	15 18	nsyl	⊢ ( ( 𝑅 Or 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
20	19	adantr	⊢ ( ( ( 𝑅 Or 𝑥 ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 𝑅 𝑧 ) → ¬ 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
21		nelne1	⊢ ( ( 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ∧ ¬ 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ≠ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } )
22	21	necomd	⊢ ( ( 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ∧ ¬ 𝑦 ∈ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ≠ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
23	14 20 22	syl2anc	⊢ ( ( ( 𝑅 Or 𝑥 ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 𝑅 𝑧 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ≠ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
24	23	adantlrr	⊢ ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑦 𝑅 𝑧 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ≠ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
25		vex	⊢ 𝑥 ∈ V
26	25	rabex	⊢ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ∈ V
27	26	brrpss	⊢ ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ↔ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ⊊ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
28		df-pss	⊢ ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ⊊ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ↔ ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ⊆ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ∧ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ≠ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ) )
29	27 28	bitri	⊢ ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ↔ ( { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ⊆ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ∧ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } ≠ { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ) )
30	10 24 29	sylanbrc	⊢ ( ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ∧ 𝑦 𝑅 𝑧 ) → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } )
31	30	ex	⊢ ( ( 𝑅 Or 𝑥 ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) → ( 𝑦 𝑅 𝑧 → { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑦 } [⊊] { 𝑤 ∈ 𝑥 ∣ 𝑤 𝑅 𝑧 } ) )