fpwwe2 - Metamath Proof Explorer

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

Theorem fpwwe2 10566

Description: Given any function 𝐹 from well-orderings of subsets of 𝐴 to 𝐴, there is a unique well-ordered subset ⟨𝑋, (𝑊‘𝑋)⟩ which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9952. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)

**Hypotheses**
Ref	Expression
fpwwe2.1	⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fpwwe2.3	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2.4	⊢ 𝑋 = ∪ dom 𝑊

**Assertion**
Ref	Expression
fpwwe2	⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))

Distinct variable groups: 𝑦,𝑢,𝑟,𝑥,𝐹 𝑋,𝑟,𝑢,𝑥,𝑦 𝜑,𝑟,𝑢,𝑥,𝑦 𝐴,𝑟,𝑥 𝑅,𝑟,𝑢,𝑥,𝑦 𝑌,𝑟,𝑢,𝑥,𝑦 𝑊,𝑟,𝑢,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑦,𝑢) 𝑉(𝑥,𝑦,𝑢,𝑟)

Proof of Theorem fpwwe2 Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwwe2.1	. . . . . . . . . . 11 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
2		fpwwe2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		fpwwe2.3	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
4		fpwwe2.4	. . . . . . . . . . 11 ⊢ 𝑋 = ∪ dom 𝑊
5	1, 2, 3, 4	fpwwe2lem10 10563	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
6	5	ffund 6672	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝑊)
7		funbrfv2b 6897	. . . . . . . . 9 ⊢ (Fun 𝑊 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊‘𝑌) = 𝑅)))
8	6, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊‘𝑌) = 𝑅)))
9	8	simprbda 498	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌𝑊𝑅) → 𝑌 ∈ dom 𝑊)
10	9	adantrr 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ∈ dom 𝑊)
11		elssuni 4881	. . . . . . 7 ⊢ (𝑌 ∈ dom 𝑊 → 𝑌 ⊆ ∪ dom 𝑊)
12	11, 4	sseqtrrdi 3963	. . . . . 6 ⊢ (𝑌 ∈ dom 𝑊 → 𝑌 ⊆ 𝑋)
13	10, 12	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ⊆ 𝑋)
14		simpl 482	. . . . . . 7 ⊢ ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋 ⊆ 𝑌)
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋 ⊆ 𝑌))
16		simplrr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑌𝐹𝑅) ∈ 𝑌)
17	2	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝐴 ∈ 𝑉)
18	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝐴 ∈ 𝑉)
19	1, 2, 3, 4	fpwwe2lem11 10564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)
20		funfvbrb 7003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
21	6, 20	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
22	19, 21	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋𝑊(𝑊‘𝑋))
23	1, 2	fpwwe2lem2 10555	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
24	22, 23	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
25	24	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
26	25	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)))
27	26	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ⊆ 𝐴)
28	18, 27	ssexd 5265	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ∈ V)
29	28	difexd 5272	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) ∈ V)
30	25	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
31	30	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) We 𝑋)
32		wefr 5621	. . . . . . . . . . . . 13 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
33	31, 32	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) Fr 𝑋)
34		difssd 4077	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) ⊆ 𝑋)
35		fri 5589	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∖ 𝑌) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑋 ∖ 𝑌) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑌) ≠ ∅)) → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
36	35	expr 456	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∖ 𝑌) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ (𝑋 ∖ 𝑌) ⊆ 𝑋) → ((𝑋 ∖ 𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧))
37	29, 33, 34, 36	syl21anc 838	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∖ 𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧))
38		ssdif0 4306	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
39		indif1 4222	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ 𝑌) ∩ (^◡(𝑊‘𝑋) “ {𝑧})) = ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌)
40	39	eqeq1i 2741	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑌) ∩ (^◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
41		disj 4390	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑌) ∩ (^◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧}))
42		vex 3433	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑤 ∈ V
43	42	eliniseg 6059	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ V → (𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧}) ↔ 𝑤(𝑊‘𝑋)𝑧))
44	43	elv 3434	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧}) ↔ 𝑤(𝑊‘𝑋)𝑧)
45	44	notbii 320	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧}) ↔ ¬ 𝑤(𝑊‘𝑋)𝑧)
46	45	ralbii 3083	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧}) ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
47	41, 46	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑌) ∩ (^◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
48	38, 40, 47	3bitr2i 299	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
49		cnvimass 6047	. . . . . . . . . . . . . . . . 17 ⊢ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ dom (𝑊‘𝑋)
50	26	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
51		dmss 5857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
53		dmxpid 5885	. . . . . . . . . . . . . . . . . 18 ⊢ dom (𝑋 × 𝑋) = 𝑋
54	52, 53	sseqtrdi 3962	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊‘𝑋) ⊆ 𝑋)
55	49, 54	sstrid 3933	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑋)
56		sseqin2 4163	. . . . . . . . . . . . . . . 16 ⊢ ((^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) = (^◡(𝑊‘𝑋) “ {𝑧}))
57	55, 56	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) = (^◡(𝑊‘𝑋) “ {𝑧}))
58	57	sseq1d 3953	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∩ (^◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
59	48, 58	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 ↔ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
60	59	rexbidv 3161	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 ↔ ∃𝑧 ∈ (𝑋 ∖ 𝑌)(^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
61		eldifn 4072	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (𝑋 ∖ 𝑌) → ¬ 𝑧 ∈ 𝑌)
62	61	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ 𝑧 ∈ 𝑌)
63		eleq1w 2819	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑌 ↔ 𝑧 ∈ 𝑌))
64	63	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑧 → (¬ 𝑤 ∈ 𝑌 ↔ ¬ 𝑧 ∈ 𝑌))
65	62, 64	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 = 𝑧 → ¬ 𝑤 ∈ 𝑌))
66	65	con2d 134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 ∈ 𝑌 → ¬ 𝑤 = 𝑧))
67	66	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑤 = 𝑧)
68	62	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑧 ∈ 𝑌)
69		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
70	69	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
71	70	breqd 5096	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 ↔ 𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤))
72		eldifi 4071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝑋 ∖ 𝑌) → 𝑧 ∈ 𝑋)
73	72	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑧 ∈ 𝑋)
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑧 ∈ 𝑋)
75		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
76		brxp 5680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × 𝑌)𝑤 ↔ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌))
77	74, 75, 76	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑧(𝑋 × 𝑌)𝑤)
78		brin 5137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ (𝑧(𝑊‘𝑋)𝑤 ∧ 𝑧(𝑋 × 𝑌)𝑤))
79	78	rbaib 538	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × 𝑌)𝑤 → (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
80	77, 79	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
81	71, 80	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
82	1, 2	fpwwe2lem2 10555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑌𝑊𝑅 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(^◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
83	82	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑌𝑊𝑅) → ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(^◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
84	83	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(^◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
85	84	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)))
86	85	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
87	86	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑅 ⊆ (𝑌 × 𝑌))
88	87	ssbrd 5128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 → 𝑧(𝑌 × 𝑌)𝑤))
89		brxp 5680	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑌 × 𝑌)𝑤 ↔ (𝑧 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌))
90	89	simplbi 496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(𝑌 × 𝑌)𝑤 → 𝑧 ∈ 𝑌)
91	88, 90	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 → 𝑧 ∈ 𝑌))
92	81, 91	sylbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧(𝑊‘𝑋)𝑤 → 𝑧 ∈ 𝑌))
93	68, 92	mtod 198	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑧(𝑊‘𝑋)𝑤)
94	31	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑊‘𝑋) We 𝑋)
95		weso 5622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑊‘𝑋) Or 𝑋)
97	13	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ 𝑋)
98	97	sselda 3921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑋)
99		sotric 5569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑤(𝑊‘𝑋)𝑧 ↔ ¬ (𝑤 = 𝑧 ∨ 𝑧(𝑊‘𝑋)𝑤)))
100		ioran 986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑤 = 𝑧 ∨ 𝑧(𝑊‘𝑋)𝑤) ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤))
101	99, 100	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑤(𝑊‘𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤)))
102	96, 98, 74, 101	syl12anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑤(𝑊‘𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤)))
103	67, 93, 102	mpbir2and 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤(𝑊‘𝑋)𝑧)
104	103, 44	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧}))
105	104	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 ∈ 𝑌 → 𝑤 ∈ (^◡(𝑊‘𝑋) “ {𝑧})))
106	105	ssrdv 3927	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ (^◡(𝑊‘𝑋) “ {𝑧}))
107		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)
108	106, 107	eqssd 3939	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 = (^◡(𝑊‘𝑋) “ {𝑧}))
109		in32 4170	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌))
110		simplrr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
111	110	ineq1d 4159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)))
112	86	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
113		dfss2 3907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ⊆ (𝑌 × 𝑌) ↔ (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
114	112, 113	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
115	111, 114	eqtr3d 2773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = 𝑅)
116		inss2 4178	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑌 × 𝑌)
117		xpss1 5650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 ⊆ 𝑋 → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
118	97, 117	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
119	116, 118	sstrid 3933	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌))
120		dfss2 3907	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌) ↔ (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
121	119, 120	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
122	109, 115, 121	3eqtr3a 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
123	108	sqxpeqd 5663	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) = ((^◡(𝑊‘𝑋) “ {𝑧}) × (^◡(𝑊‘𝑋) “ {𝑧})))
124	123	ineq2d 4160	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑧}) × (^◡(𝑊‘𝑋) “ {𝑧}))))
125	122, 124	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑧}) × (^◡(𝑊‘𝑋) “ {𝑧}))))
126	108, 125	oveq12d 7385	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = ((^◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑧}) × (^◡(𝑊‘𝑋) “ {𝑧})))))
127	18	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝐴 ∈ 𝑉)
128	22	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊(𝑊‘𝑋))
129	128	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑋𝑊(𝑊‘𝑋))
130	1, 127, 129	fpwwe2lem3 10556	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑧 ∈ 𝑋) → ((^◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑧}) × (^◡(𝑊‘𝑋) “ {𝑧})))) = 𝑧)
131	73, 130	mpdan 688	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((^◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((^◡(𝑊‘𝑋) “ {𝑧}) × (^◡(𝑊‘𝑋) “ {𝑧})))) = 𝑧)
132	126, 131	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = 𝑧)
133	132, 62	eqneltrd 2856	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ (𝑌𝐹𝑅) ∈ 𝑌)
134	133	rexlimdvaa 3139	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)(^◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
135	60, 134	sylbid 240	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
136	37, 135	syld 47	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∖ 𝑌) ≠ ∅ → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
137	136	necon4ad 2951	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑌𝐹𝑅) ∈ 𝑌 → (𝑋 ∖ 𝑌) = ∅))
138	16, 137	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) = ∅)
139		ssdif0 4306	. . . . . . . 8 ⊢ (𝑋 ⊆ 𝑌 ↔ (𝑋 ∖ 𝑌) = ∅)
140	138, 139	sylibr 234	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ⊆ 𝑌)
141	140	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌))) → 𝑋 ⊆ 𝑌))
142	3	adantlr 716	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
143		simprl 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑊𝑅)
144	1, 17, 142, 128, 143	fpwwe2lem9 10562	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) ∨ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))))
145	15, 141, 144	mpjaod 861	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋 ⊆ 𝑌)
146	13, 145	eqssd 3939	. . . 4 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 = 𝑋)
147	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → Fun 𝑊)
148	146, 143	eqbrtrrd 5109	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊𝑅)
149		funbrfv 6888	. . . . . 6 ⊢ (Fun 𝑊 → (𝑋𝑊𝑅 → (𝑊‘𝑋) = 𝑅))
150	147, 148, 149	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑊‘𝑋) = 𝑅)
151	150	eqcomd 2742	. . . 4 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 = (𝑊‘𝑋))
152	146, 151	jca 511	. . 3 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))
153	152	ex 412	. 2 ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) → (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))
154	1, 2, 3, 4	fpwwe2lem12 10565	. . . 4 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
155	22, 154	jca 511	. . 3 ⊢ (𝜑 → (𝑋𝑊(𝑊‘𝑋) ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
156		breq12 5090	. . . 4 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝑊𝑅 ↔ 𝑋𝑊(𝑊‘𝑋)))
157		oveq12 7376	. . . . 5 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝐹𝑅) = (𝑋𝐹(𝑊‘𝑋)))
158		simpl 482	. . . . 5 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → 𝑌 = 𝑋)
159	157, 158	eleq12d 2830	. . . 4 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → ((𝑌𝐹𝑅) ∈ 𝑌 ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
160	156, 159	anbi12d 633	. . 3 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑋𝑊(𝑊‘𝑋) ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)))
161	155, 160	syl5ibrcom 247	. 2 ⊢ (𝜑 → ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)))
162	153, 161	impbid 212	1 ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∀wral 3051 ∃wrex 3061 Vcvv 3429 [wsbc 3728 ∖ cdif 3886 ∩ cin 3888 ⊆ wss 3889 ∅c0 4273 𝒫 cpw 4541 {csn 4567 ∪ cuni 4850 class class class wbr 5085 {copab 5147 Or wor 5538 Fr wfr 5581 We wwe 5583 × cxp 5629 ^◡ccnv 5630 dom cdm 5631 “ cima 5634 Fun wfun 6492 ‘cfv 6498 (class class class)co 7367

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-oi 9425

This theorem is referenced by: fpwwe 10569 canthwelem 10573 pwfseqlem4 10585

W3C validator