Metamath Proof Explorer

Theorem wemapsolem

Description: Lemma for wemapso . (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypotheses wemapso.t ⊢ T = x y | ∃ z ∈ A x ⁡ z S y ⁡ z ∧ ∀ w ∈ A w R z → x ⁡ w = y ⁡ w
wemapsolem.1 ⊢ U ⊆ B A
wemapsolem.2 ⊢ φ → R Or A
wemapsolem.3 ⊢ φ → S Or B
wemapsolem.4 ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∃ c ∈ dom ⁡ a ∖ b ∀ d ∈ dom ⁡ a ∖ b ¬ d R c
Assertion wemapsolem ⊢ φ → T Or U

Proof

Step Hyp Ref Expression
1 wemapso.t ⊢ T = x y | ∃ z ∈ A x ⁡ z S y ⁡ z ∧ ∀ w ∈ A w R z → x ⁡ w = y ⁡ w
2 wemapsolem.1 ⊢ U ⊆ B A
3 wemapsolem.2 ⊢ φ → R Or A
4 wemapsolem.3 ⊢ φ → S Or B
5 wemapsolem.4 ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∃ c ∈ dom ⁡ a ∖ b ∀ d ∈ dom ⁡ a ∖ b ¬ d R c
6 sopo ⊢ S Or B → S Po B
7 4 6 syl ⊢ φ → S Po B
8 1 wemappo ⊢ R Or A ∧ S Po B → T Po B A
9 3 7 8 syl2anc ⊢ φ → T Po B A
10 poss ⊢ U ⊆ B A → T Po B A → T Po U
11 2 9 10 mpsyl ⊢ φ → T Po U
12 df-ne ⊢ a ≠ b ↔ ¬ a = b
13 simprll ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → a ∈ U
14 2 13 sselid ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → a ∈ B A
15 elmapi ⊢ a ∈ B A → a : A ⟶ B
16 14 15 syl ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → a : A ⟶ B
17 16 ffnd ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → a Fn A
18 simprlr ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → b ∈ U
19 2 18 sselid ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → b ∈ B A
20 elmapi ⊢ b ∈ B A → b : A ⟶ B
21 19 20 syl ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → b : A ⟶ B
22 21 ffnd ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → b Fn A
23 fndmdif ⊢ a Fn A ∧ b Fn A → dom ⁡ a ∖ b = x ∈ A | a ⁡ x ≠ b ⁡ x
24 17 22 23 syl2anc ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → dom ⁡ a ∖ b = x ∈ A | a ⁡ x ≠ b ⁡ x
25 24 eleq2d ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → c ∈ dom ⁡ a ∖ b ↔ c ∈ x ∈ A | a ⁡ x ≠ b ⁡ x
26 nesym ⊢ a ⁡ x ≠ b ⁡ x ↔ ¬ b ⁡ x = a ⁡ x
27 fveq2 ⊢ x = c → b ⁡ x = b ⁡ c
28 fveq2 ⊢ x = c → a ⁡ x = a ⁡ c
29 27 28 eqeq12d ⊢ x = c → b ⁡ x = a ⁡ x ↔ b ⁡ c = a ⁡ c
30 29 notbid ⊢ x = c → ¬ b ⁡ x = a ⁡ x ↔ ¬ b ⁡ c = a ⁡ c
31 26 30 bitrid ⊢ x = c → a ⁡ x ≠ b ⁡ x ↔ ¬ b ⁡ c = a ⁡ c
32 31 elrab ⊢ c ∈ x ∈ A | a ⁡ x ≠ b ⁡ x ↔ c ∈ A ∧ ¬ b ⁡ c = a ⁡ c
33 25 32 bitrdi ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → c ∈ dom ⁡ a ∖ b ↔ c ∈ A ∧ ¬ b ⁡ c = a ⁡ c
34 24 eleq2d ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → d ∈ dom ⁡ a ∖ b ↔ d ∈ x ∈ A | a ⁡ x ≠ b ⁡ x
35 fveq2 ⊢ x = d → b ⁡ x = b ⁡ d
36 fveq2 ⊢ x = d → a ⁡ x = a ⁡ d
37 35 36 eqeq12d ⊢ x = d → b ⁡ x = a ⁡ x ↔ b ⁡ d = a ⁡ d
38 37 notbid ⊢ x = d → ¬ b ⁡ x = a ⁡ x ↔ ¬ b ⁡ d = a ⁡ d
39 26 38 bitrid ⊢ x = d → a ⁡ x ≠ b ⁡ x ↔ ¬ b ⁡ d = a ⁡ d
40 39 elrab ⊢ d ∈ x ∈ A | a ⁡ x ≠ b ⁡ x ↔ d ∈ A ∧ ¬ b ⁡ d = a ⁡ d
41 34 40 bitrdi ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → d ∈ dom ⁡ a ∖ b ↔ d ∈ A ∧ ¬ b ⁡ d = a ⁡ d
42 41 imbi1d ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → d ∈ dom ⁡ a ∖ b → ¬ d R c ↔ d ∈ A ∧ ¬ b ⁡ d = a ⁡ d → ¬ d R c
43 impexp ⊢ d ∈ A ∧ ¬ b ⁡ d = a ⁡ d → ¬ d R c ↔ d ∈ A → ¬ b ⁡ d = a ⁡ d → ¬ d R c
44 con34b ⊢ d R c → b ⁡ d = a ⁡ d ↔ ¬ b ⁡ d = a ⁡ d → ¬ d R c
45 44 imbi2i ⊢ d ∈ A → d R c → b ⁡ d = a ⁡ d ↔ d ∈ A → ¬ b ⁡ d = a ⁡ d → ¬ d R c
46 43 45 bitr4i ⊢ d ∈ A ∧ ¬ b ⁡ d = a ⁡ d → ¬ d R c ↔ d ∈ A → d R c → b ⁡ d = a ⁡ d
47 42 46 bitrdi ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → d ∈ dom ⁡ a ∖ b → ¬ d R c ↔ d ∈ A → d R c → b ⁡ d = a ⁡ d
48 47 ralbidv2 ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∀ d ∈ dom ⁡ a ∖ b ¬ d R c ↔ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
49 33 48 anbi12d ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → c ∈ dom ⁡ a ∖ b ∧ ∀ d ∈ dom ⁡ a ∖ b ¬ d R c ↔ c ∈ A ∧ ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
50 anass ⊢ c ∈ A ∧ ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ↔ c ∈ A ∧ ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
51 49 50 bitrdi ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → c ∈ dom ⁡ a ∖ b ∧ ∀ d ∈ dom ⁡ a ∖ b ¬ d R c ↔ c ∈ A ∧ ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
52 51 rexbidv2 ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∃ c ∈ dom ⁡ a ∖ b ∀ d ∈ dom ⁡ a ∖ b ¬ d R c ↔ ∃ c ∈ A ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
53 5 52 mpbid ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∃ c ∈ A ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
54 4 ad2antrr ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b ∧ c ∈ A → S Or B
55 21 ffvelcdmda ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b ∧ c ∈ A → b ⁡ c ∈ B
56 16 ffvelcdmda ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b ∧ c ∈ A → a ⁡ c ∈ B
57 sotrieq ⊢ S Or B ∧ b ⁡ c ∈ B ∧ a ⁡ c ∈ B → b ⁡ c = a ⁡ c ↔ ¬ b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c
58 57 con2bid ⊢ S Or B ∧ b ⁡ c ∈ B ∧ a ⁡ c ∈ B → b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ↔ ¬ b ⁡ c = a ⁡ c
59 58 biimprd ⊢ S Or B ∧ b ⁡ c ∈ B ∧ a ⁡ c ∈ B → ¬ b ⁡ c = a ⁡ c → b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c
60 54 55 56 59 syl12anc ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b ∧ c ∈ A → ¬ b ⁡ c = a ⁡ c → b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c
61 60 anim1d ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b ∧ c ∈ A → ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d → b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
62 61 reximdva ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∃ c ∈ A ¬ b ⁡ c = a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d → ∃ c ∈ A b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
63 53 62 mpd ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → ∃ c ∈ A b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
64 1 wemaplem1 ⊢ b ∈ V ∧ a ∈ V → b T a ↔ ∃ c ∈ A b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
65 64 el2v ⊢ b T a ↔ ∃ c ∈ A b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
66 1 wemaplem1 ⊢ a ∈ V ∧ b ∈ V → a T b ↔ ∃ c ∈ A a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
67 66 el2v ⊢ a T b ↔ ∃ c ∈ A a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
68 65 67 orbi12i ⊢ b T a ∨ a T b ↔ ∃ c ∈ A b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ ∃ c ∈ A a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
69 r19.43 ⊢ ∃ c ∈ A b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d ↔ ∃ c ∈ A b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ ∃ c ∈ A a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
70 andir ⊢ b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ↔ b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
71 eqcom ⊢ b ⁡ d = a ⁡ d ↔ a ⁡ d = b ⁡ d
72 71 imbi2i ⊢ d R c → b ⁡ d = a ⁡ d ↔ d R c → a ⁡ d = b ⁡ d
73 72 ralbii ⊢ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ↔ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
74 73 anbi2i ⊢ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ↔ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
75 74 orbi2i ⊢ b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ↔ b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d
76 70 75 bitr2i ⊢ b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d ↔ b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
77 76 rexbii ⊢ ∃ c ∈ A b ⁡ c S a ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → a ⁡ d = b ⁡ d ↔ ∃ c ∈ A b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
78 68 69 77 3bitr2i ⊢ b T a ∨ a T b ↔ ∃ c ∈ A b ⁡ c S a ⁡ c ∨ a ⁡ c S b ⁡ c ∧ ∀ d ∈ A d R c → b ⁡ d = a ⁡ d
79 63 78 sylibr ⊢ φ ∧ a ∈ U ∧ b ∈ U ∧ a ≠ b → b T a ∨ a T b
80 79 expr ⊢ φ ∧ a ∈ U ∧ b ∈ U → a ≠ b → b T a ∨ a T b
81 12 80 biimtrrid ⊢ φ ∧ a ∈ U ∧ b ∈ U → ¬ a = b → b T a ∨ a T b
82 81 orrd ⊢ φ ∧ a ∈ U ∧ b ∈ U → a = b ∨ b T a ∨ a T b
83 3orrot ⊢ a T b ∨ a = b ∨ b T a ↔ a = b ∨ b T a ∨ a T b
84 3orass ⊢ a = b ∨ b T a ∨ a T b ↔ a = b ∨ b T a ∨ a T b
85 83 84 bitr2i ⊢ a = b ∨ b T a ∨ a T b ↔ a T b ∨ a = b ∨ b T a
86 82 85 sylib ⊢ φ ∧ a ∈ U ∧ b ∈ U → a T b ∨ a = b ∨ b T a
87 11 86 issod ⊢ φ → T Or U