Metamath Proof Explorer

Theorem wemapsolem

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

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