Metamath Proof Explorer

Theorem fin2solem

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

Ref Expression
Assertion fin2solem ⊢ROrx∧y∈x∧z∈x→yRz→w∈x|wRy[⊂]w∈x|wRz

Proof

Step Hyp Ref Expression
1 ancom ⊢y∈x∧z∈x∧w∈x↔w∈x∧y∈x∧z∈x
2 3anass ⊢w∈x∧y∈x∧z∈x↔w∈x∧y∈x∧z∈x
3 1 2 bitr4i ⊢y∈x∧z∈x∧w∈x↔w∈x∧y∈x∧z∈x
4 sotr ⊢ROrx∧w∈x∧y∈x∧z∈x→wRy∧yRz→wRz
5 3 4 sylan2b ⊢ROrx∧y∈x∧z∈x∧w∈x→wRy∧yRz→wRz
6 5 anassrs ⊢ROrx∧y∈x∧z∈x∧w∈x→wRy∧yRz→wRz
7 6 ancomsd ⊢ROrx∧y∈x∧z∈x∧w∈x→yRz∧wRy→wRz
8 7 expdimp ⊢ROrx∧y∈x∧z∈x∧w∈x∧yRz→wRy→wRz
9 8 an32s ⊢ROrx∧y∈x∧z∈x∧yRz∧w∈x→wRy→wRz
10 9 ss2rabdv ⊢ROrx∧y∈x∧z∈x∧yRz→w∈x|wRy⊆w∈x|wRz
11 breq1 ⊢w=y→wRz↔yRz
12 11 elrab ⊢y∈w∈x|wRz↔y∈x∧yRz
13 12 biimpri ⊢y∈x∧yRz→y∈w∈x|wRz
14 13 adantll ⊢ROrx∧y∈x∧yRz→y∈w∈x|wRz
15 sonr ⊢ROrx∧y∈x→¬yRy
16 breq1 ⊢w=y→wRy↔yRy
17 16 elrab ⊢y∈w∈x|wRy↔y∈x∧yRy
18 17 simprbi ⊢y∈w∈x|wRy→yRy
19 15 18 nsyl ⊢ROrx∧y∈x→¬y∈w∈x|wRy
20 19 adantr ⊢ROrx∧y∈x∧yRz→¬y∈w∈x|wRy
21 nelne1 ⊢y∈w∈x|wRz∧¬y∈w∈x|wRy→w∈x|wRz≠w∈x|wRy
22 21 necomd ⊢y∈w∈x|wRz∧¬y∈w∈x|wRy→w∈x|wRy≠w∈x|wRz
23 14 20 22 syl2anc ⊢ROrx∧y∈x∧yRz→w∈x|wRy≠w∈x|wRz
24 23 adantlrr ⊢ROrx∧y∈x∧z∈x∧yRz→w∈x|wRy≠w∈x|wRz
25 vex ⊢x∈V
26 25 rabex ⊢w∈x|wRz∈V
27 26 brrpss ⊢w∈x|wRy[⊂]w∈x|wRz↔w∈x|wRy⊂w∈x|wRz
28 df-pss ⊢w∈x|wRy⊂w∈x|wRz↔w∈x|wRy⊆w∈x|wRz∧w∈x|wRy≠w∈x|wRz
29 27 28 bitri ⊢w∈x|wRy[⊂]w∈x|wRz↔w∈x|wRy⊆w∈x|wRz∧w∈x|wRy≠w∈x|wRz
30 10 24 29 sylanbrc ⊢ROrx∧y∈x∧z∈x∧yRz→w∈x|wRy[⊂]w∈x|wRz
31 30 ex ⊢ROrx∧y∈x∧z∈x→yRz→w∈x|wRy[⊂]w∈x|wRz