wemapsolem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wemapsolem		Structured version Visualization version GIF version

Theorem wemapsolem 8998

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

**Hypotheses**
Ref	Expression
wemapso.t	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
wemapsolem.1	⊢ 𝑈 ⊆ (𝐵 ↑_m 𝐴)
wemapsolem.2	⊢ (𝜑 → 𝐴 ∈ V)
wemapsolem.3	⊢ (𝜑 → 𝑅 Or 𝐴)
wemapsolem.4	⊢ (𝜑 → 𝑆 Or 𝐵)
wemapsolem.5	⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)

**Assertion**
Ref	Expression
wemapsolem	⊢ (𝜑 → 𝑇 Or 𝑈)

Distinct variable groups: 𝑎,𝑏,𝑐,𝑑,𝑥,𝐵 𝑇,𝑎,𝑏,𝑐,𝑑 𝑈,𝑎,𝑏,𝑐,𝑑 𝑤,𝑎,𝑦,𝑧,𝑏,𝑐,𝑥,𝐴,𝑑 𝑅,𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧 𝑆,𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧 𝜑,𝑎,𝑏,𝑐,𝑑 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑧,𝑤) 𝐵(𝑦,𝑧,𝑤) 𝑇(𝑥,𝑦,𝑧,𝑤) 𝑈(𝑥,𝑦,𝑧,𝑤)

**Proof of Theorem wemapsolem**
Step	Hyp	Ref	Expression
1		wemapsolem.1	. . 3 ⊢ 𝑈 ⊆ (𝐵 ↑_m 𝐴)
2		wemapsolem.2	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
3		wemapsolem.3	. . . 4 ⊢ (𝜑 → 𝑅 Or 𝐴)
4		wemapsolem.4	. . . . 5 ⊢ (𝜑 → 𝑆 Or 𝐵)
5		sopo 5456	. . . . 5 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → 𝑆 Po 𝐵)
7		wemapso.t	. . . . 5 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
8	7	wemappo 8997	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑_m 𝐴))
9	2, 3, 6, 8	syl3anc 1368	. . 3 ⊢ (𝜑 → 𝑇 Po (𝐵 ↑_m 𝐴))
10		poss 5440	. . 3 ⊢ (𝑈 ⊆ (𝐵 ↑_m 𝐴) → (𝑇 Po (𝐵 ↑_m 𝐴) → 𝑇 Po 𝑈))
11	1, 9, 10	mpsyl 68	. 2 ⊢ (𝜑 → 𝑇 Po 𝑈)
12		df-ne 2988	. . . . 5 ⊢ (𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏)
13		wemapsolem.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)
14		simprll 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝑈)
15	1, 14	sseldi 3913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑_m 𝐴))
16		elmapi 8411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝐵 ↑_m 𝐴) → 𝑎:𝐴⟶𝐵)
17	15, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵)
18	17	ffnd 6488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴)
19		simprlr 779	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝑈)
20	1, 19	sseldi 3913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑_m 𝐴))
21		elmapi 8411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝐵 ↑_m 𝐴) → 𝑏:𝐴⟶𝐵)
22	20, 21	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵)
23	22	ffnd 6488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴)
24		fndmdif 6789	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
25	18, 23, 24	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
26	25	eleq2d 2875	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
27		nesym 3043	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑥) = (𝑎‘𝑥))
28		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑏‘𝑥) = (𝑏‘𝑐))
29		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑎‘𝑥) = (𝑎‘𝑐))
30	28, 29	eqeq12d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑐 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑐) = (𝑎‘𝑐)))
31	30	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑐 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
32	27, 31	syl5bb 286	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑐 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
33	32	elrab 3628	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
34	26, 33	syl6bb 290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐))))
35	25	eleq2d 2875	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
36		fveq2 6645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑏‘𝑥) = (𝑏‘𝑑))
37		fveq2 6645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑎‘𝑥) = (𝑎‘𝑑))
38	36, 37	eqeq12d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑑 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑑) = (𝑎‘𝑑)))
39	38	notbid 321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑑 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
40	27, 39	syl5bb 286	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑑 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
41	40	elrab 3628	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
42	35, 41	syl6bb 290	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑))))
43	42	imbi1d 345	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐)))
44		impexp 454	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
45		con34b 319	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐))
46	45	imbi2i 339	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
47	44, 46	bitr4i 281	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
48	43, 47	syl6bb 290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
49	48	ralbidv2 3160	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
50	34, 49	anbi12d 633	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
51		anass 472	. . . . . . . . . . 11 ⊢ (((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
52	50, 51	syl6bb 290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))))
53	52	rexbidv2 3254	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
54	13, 53	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
55	4	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑆 Or 𝐵)
56	22	ffvelrnda 6828	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑏‘𝑐) ∈ 𝐵)
57	17	ffvelrnda 6828	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑎‘𝑐) ∈ 𝐵)
58		sotrieq 5466	. . . . . . . . . . . . 13 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → ((𝑏‘𝑐) = (𝑎‘𝑐) ↔ ¬ ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
59	58	con2bid 358	. . . . . . . . . . . 12 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
60	59	biimprd 251	. . . . . . . . . . 11 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
61	55, 56, 57, 60	syl12anc 835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
62	61	anim1d 613	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
63	62	reximdva 3233	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
64	54, 63	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
65	7	wemaplem1 8994	. . . . . . . . . 10 ⊢ ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
66	65	el2v 3448	. . . . . . . . 9 ⊢ (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
67	7	wemaplem1 8994	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
68	67	el2v 3448	. . . . . . . . 9 ⊢ (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
69	66, 68	orbi12i 912	. . . . . . . 8 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
70		r19.43 3304	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
71		andir 1006	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
72		eqcom 2805	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑑) = (𝑎‘𝑑) ↔ (𝑎‘𝑑) = (𝑏‘𝑑))
73	72	imbi2i 339	. . . . . . . . . . . . 13 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
74	73	ralbii 3133	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
75	74	anbi2i 625	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
76	75	orbi2i 910	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
77	71, 76	bitr2i 279	. . . . . . . . 9 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
78	77	rexbii 3210	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
79	69, 70, 78	3bitr2i 302	. . . . . . 7 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
80	64, 79	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
81	80	expr 460	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 ≠ 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
82	12, 81	syl5bir 246	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
83	82	orrd 860	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
84		3orrot 1089	. . . 4 ⊢ ((𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎) ↔ (𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
85		3orass 1087	. . . 4 ⊢ ((𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
86	84, 85	bitr2i 279	. . 3 ⊢ ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
87	83, 86	sylib 221	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
88	11, 87	issod 5470	1 ⊢ (𝜑 → 𝑇 Or 𝑈)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 {crab 3110 Vcvv 3441 ∖ cdif 3878 ⊆ wss 3881 class class class wbr 5030 {copab 5092 Po wpo 5436 Or wor 5437 dom cdm 5519 Fn wfn 6319 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ↑_m cmap 8389

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-1st 7671 df-2nd 7672 df-map 8391

This theorem is referenced by: wemapso 8999 wemapso2lem 9000

W3C validator