Metamath Proof Explorer

Theorem sprsymrelfolem2

Description: Lemma 2 for sprsymrelfo . (Contributed by AV, 23-Nov-2021)

Ref Expression
Hypothesis sprsymrelfo.q ⊢ Q = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b
Assertion sprsymrelfolem2 ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y ↔ ∃ c ∈ Q c = x y

Proof

Step Hyp Ref Expression
1 sprsymrelfo.q ⊢ Q = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b
2 df-br ⊢ x R y ↔ x y ∈ R
3 simpl ⊢ V ∈ W ∧ R ⊆ V × V → V ∈ W
4 ssel ⊢ R ⊆ V × V → x y ∈ R → x y ∈ V × V
5 4 adantl ⊢ V ∈ W ∧ R ⊆ V × V → x y ∈ R → x y ∈ V × V
6 5 imp ⊢ V ∈ W ∧ R ⊆ V × V ∧ x y ∈ R → x y ∈ V × V
7 opelxp ⊢ x y ∈ V × V ↔ x ∈ V ∧ y ∈ V
8 6 7 sylib ⊢ V ∈ W ∧ R ⊆ V × V ∧ x y ∈ R → x ∈ V ∧ y ∈ V
9 prelspr ⊢ V ∈ W ∧ x ∈ V ∧ y ∈ V → x y ∈ Pairs ⁡ V
10 3 8 9 syl2an2r ⊢ V ∈ W ∧ R ⊆ V × V ∧ x y ∈ R → x y ∈ Pairs ⁡ V
11 10 ex ⊢ V ∈ W ∧ R ⊆ V × V → x y ∈ R → x y ∈ Pairs ⁡ V
12 2 11 syl5bi ⊢ V ∈ W ∧ R ⊆ V × V → x R y → x y ∈ Pairs ⁡ V
13 12 3adant3 ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y → x y ∈ Pairs ⁡ V
14 13 imp ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → x y ∈ Pairs ⁡ V
15 vex ⊢ x ∈ V
16 vex ⊢ y ∈ V
17 vex ⊢ a ∈ V
18 vex ⊢ b ∈ V
19 15 16 17 18 preq12b ⊢ x y = a b ↔ x = a ∧ y = b ∨ x = b ∧ y = a
20 breq12 ⊢ x = a ∧ y = b → x R y ↔ a R b
21 20 biimpd ⊢ x = a ∧ y = b → x R y → a R b
22 21 com12 ⊢ x R y → x = a ∧ y = b → a R b
23 22 adantl ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → x = a ∧ y = b → a R b
24 23 adantr ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y ∧ a ∈ V ∧ b ∈ V → x = a ∧ y = b → a R b
25 24 com12 ⊢ x = a ∧ y = b → V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y ∧ a ∈ V ∧ b ∈ V → a R b
26 rsp2 ⊢ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x ∈ V ∧ y ∈ V → x R y ↔ y R x
27 26 ancomsd ⊢ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → y ∈ V ∧ x ∈ V → x R y ↔ y R x
28 27 imp ⊢ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ y ∈ V ∧ x ∈ V → x R y ↔ y R x
29 28 biimpd ⊢ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ y ∈ V ∧ x ∈ V → x R y → y R x
30 29 ex ⊢ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → y ∈ V ∧ x ∈ V → x R y → y R x
31 30 3ad2ant3 ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → y ∈ V ∧ x ∈ V → x R y → y R x
32 31 com23 ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y → y ∈ V ∧ x ∈ V → y R x
33 32 imp ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → y ∈ V ∧ x ∈ V → y R x
34 33 adantl ⊢ x = b ∧ y = a ∧ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → y ∈ V ∧ x ∈ V → y R x
35 eleq1 ⊢ y = a → y ∈ V ↔ a ∈ V
36 eleq1 ⊢ x = b → x ∈ V ↔ b ∈ V
37 35 36 bi2anan9r ⊢ x = b ∧ y = a → y ∈ V ∧ x ∈ V ↔ a ∈ V ∧ b ∈ V
38 breq12 ⊢ y = a ∧ x = b → y R x ↔ a R b
39 38 ancoms ⊢ x = b ∧ y = a → y R x ↔ a R b
40 37 39 imbi12d ⊢ x = b ∧ y = a → y ∈ V ∧ x ∈ V → y R x ↔ a ∈ V ∧ b ∈ V → a R b
41 40 adantr ⊢ x = b ∧ y = a ∧ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → y ∈ V ∧ x ∈ V → y R x ↔ a ∈ V ∧ b ∈ V → a R b
42 34 41 mpbid ⊢ x = b ∧ y = a ∧ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → a ∈ V ∧ b ∈ V → a R b
43 42 expimpd ⊢ x = b ∧ y = a → V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y ∧ a ∈ V ∧ b ∈ V → a R b
44 25 43 jaoi ⊢ x = a ∧ y = b ∨ x = b ∧ y = a → V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y ∧ a ∈ V ∧ b ∈ V → a R b
45 44 com12 ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y ∧ a ∈ V ∧ b ∈ V → x = a ∧ y = b ∨ x = b ∧ y = a → a R b
46 19 45 syl5bi ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y ∧ a ∈ V ∧ b ∈ V → x y = a b → a R b
47 46 ralrimivva ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → ∀ a ∈ V ∀ b ∈ V x y = a b → a R b
48 1 eleq2i ⊢ x y ∈ Q ↔ x y ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b
49 eqeq1 ⊢ q = x y → q = a b ↔ x y = a b
50 49 imbi1d ⊢ q = x y → q = a b → a R b ↔ x y = a b → a R b
51 50 2ralbidv ⊢ q = x y → ∀ a ∈ V ∀ b ∈ V q = a b → a R b ↔ ∀ a ∈ V ∀ b ∈ V x y = a b → a R b
52 51 elrab ⊢ x y ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b ↔ x y ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V x y = a b → a R b
53 48 52 bitri ⊢ x y ∈ Q ↔ x y ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V x y = a b → a R b
54 14 47 53 sylanbrc ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → x y ∈ Q
55 eqidd ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → x y = x y
56 eqeq1 ⊢ c = x y → c = x y ↔ x y = x y
57 56 rspcev ⊢ x y ∈ Q ∧ x y = x y → ∃ c ∈ Q c = x y
58 54 55 57 syl2anc ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x ∧ x R y → ∃ c ∈ Q c = x y
59 58 ex ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y → ∃ c ∈ Q c = x y
60 1 eleq2i ⊢ c ∈ Q ↔ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b
61 eqeq1 ⊢ q = c → q = a b ↔ c = a b
62 61 imbi1d ⊢ q = c → q = a b → a R b ↔ c = a b → a R b
63 62 2ralbidv ⊢ q = c → ∀ a ∈ V ∀ b ∈ V q = a b → a R b ↔ ∀ a ∈ V ∀ b ∈ V c = a b → a R b
64 63 elrab ⊢ c ∈ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b ↔ c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b
65 60 64 bitri ⊢ c ∈ Q ↔ c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b
66 eleq1 ⊢ c = x y → c ∈ Pairs ⁡ V ↔ x y ∈ Pairs ⁡ V
67 prsprel ⊢ x y ∈ Pairs ⁡ V ∧ x ∈ V ∧ y ∈ V → x ∈ V ∧ y ∈ V
68 15 16 67 mpanr12 ⊢ x y ∈ Pairs ⁡ V → x ∈ V ∧ y ∈ V
69 66 68 syl6bi ⊢ c = x y → c ∈ Pairs ⁡ V → x ∈ V ∧ y ∈ V
70 69 com12 ⊢ c ∈ Pairs ⁡ V → c = x y → x ∈ V ∧ y ∈ V
71 70 adantr ⊢ c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b → c = x y → x ∈ V ∧ y ∈ V
72 71 imp ⊢ c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b ∧ c = x y → x ∈ V ∧ y ∈ V
73 preq1 ⊢ a = x → a b = x b
74 73 eqeq2d ⊢ a = x → c = a b ↔ c = x b
75 breq1 ⊢ a = x → a R b ↔ x R b
76 74 75 imbi12d ⊢ a = x → c = a b → a R b ↔ c = x b → x R b
77 preq2 ⊢ b = y → x b = x y
78 77 eqeq2d ⊢ b = y → c = x b ↔ c = x y
79 breq2 ⊢ b = y → x R b ↔ x R y
80 78 79 imbi12d ⊢ b = y → c = x b → x R b ↔ c = x y → x R y
81 76 80 rspc2v ⊢ x ∈ V ∧ y ∈ V → ∀ a ∈ V ∀ b ∈ V c = a b → a R b → c = x y → x R y
82 81 a1d ⊢ x ∈ V ∧ y ∈ V → c ∈ Pairs ⁡ V → ∀ a ∈ V ∀ b ∈ V c = a b → a R b → c = x y → x R y
83 82 imp4c ⊢ x ∈ V ∧ y ∈ V → c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b ∧ c = x y → x R y
84 72 83 mpcom ⊢ c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b ∧ c = x y → x R y
85 84 a1d ⊢ c ∈ Pairs ⁡ V ∧ ∀ a ∈ V ∀ b ∈ V c = a b → a R b ∧ c = x y → V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y
86 65 85 sylanb ⊢ c ∈ Q ∧ c = x y → V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y
87 86 rexlimiva ⊢ ∃ c ∈ Q c = x y → V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y
88 87 com12 ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → ∃ c ∈ Q c = x y → x R y
89 59 88 impbid ⊢ V ∈ W ∧ R ⊆ V × V ∧ ∀ x ∈ V ∀ y ∈ V x R y ↔ y R x → x R y ↔ ∃ c ∈ Q c = x y