Theorem fpwwe2 10552

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 9938. 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 10549	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
6	5	ffund 6664	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝑊)
7		funbrfv2b 6889	. . . . . . . . 9 ⊢ (Fun 𝑊 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊‘𝑌) = 𝑅)))
8	6, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊‘𝑌) = 𝑅)))
9	8	simprbda 498	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌𝑊𝑅) → 𝑌 ∈ dom 𝑊)
10	9	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ∈ dom 𝑊)
11		elssuni 4892	. . . . . . 7 ⊢ (𝑌 ∈ dom 𝑊 → 𝑌 ⊆ ∪ dom 𝑊)
12	11, 4	sseqtrrdi 3973	. . . . . 6 ⊢ (𝑌 ∈ dom 𝑊 → 𝑌 ⊆ 𝑋)
13	10, 12	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ⊆ 𝑋)
14		simpl 482	. . . . . . 7 ⊢ ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋 ⊆ 𝑌)
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋 ⊆ 𝑌))
16		simplrr 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑌𝐹𝑅) ∈ 𝑌)
17	2	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝐴 ∈ 𝑉)
18	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝐴 ∈ 𝑉)
19	1, 2, 3, 4	fpwwe2lem11 10550	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)
20		funfvbrb 6994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
21	6, 20	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
22	19, 21	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋𝑊(𝑊‘𝑋))
23	1, 2	fpwwe2lem2 10541	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
24	22, 23	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
25	24	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
26	25	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)))
27	26	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ⊆ 𝐴)
28	18, 27	ssexd 5267	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ∈ V)
29	28	difexd 5274	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) ∈ V)
30	25	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
31	30	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) We 𝑋)
32		wefr 5612	. . . . . . . . . . . . 13 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
33	31, 32	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) Fr 𝑋)
34		difssd 4087	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) ⊆ 𝑋)
35		fri 5580	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∖ 𝑌) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑋 ∖ 𝑌) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑌) ≠ ∅)) → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
36	35	expr 456	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∖ 𝑌) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ (𝑋 ∖ 𝑌) ⊆ 𝑋) → ((𝑋 ∖ 𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧))
37	29, 33, 34, 36	syl21anc 837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∖ 𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧))
38		ssdif0 4316	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
39		indif1 4232	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌)
40	39	eqeq1i 2739	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
41		disj 4400	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}))
42		vex 3442	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑤 ∈ V
43	42	eliniseg 6051	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ V → (𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ 𝑤(𝑊‘𝑋)𝑧))
44	43	elv 3443	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ 𝑤(𝑊‘𝑋)𝑧)
45	44	notbii 320	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ ¬ 𝑤(𝑊‘𝑋)𝑧)
46	45	ralbii 3080	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
47	41, 46	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
48	38, 40, 47	3bitr2i 299	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
49		cnvimass 6039	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ dom (𝑊‘𝑋)
50	26	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
51		dmss 5849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
53		dmxpid 5877	. . . . . . . . . . . . . . . . . 18 ⊢ dom (𝑋 × 𝑋) = 𝑋
54	52, 53	sseqtrdi 3972	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊‘𝑋) ⊆ 𝑋)
55	49, 54	sstrid 3943	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑋)
56		sseqin2 4173	. . . . . . . . . . . . . . . 16 ⊢ ((◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑋 ↔ (𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) = (◡(𝑊‘𝑋) “ {𝑧}))
57	55, 56	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) = (◡(𝑊‘𝑋) “ {𝑧}))
58	57	sseq1d 3963	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
59	48, 58	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 ↔ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
60	59	rexbidv 3158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 ↔ ∃𝑧 ∈ (𝑋 ∖ 𝑌)(◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
61		eldifn 4082	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (𝑋 ∖ 𝑌) → ¬ 𝑧 ∈ 𝑌)
62	61	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ 𝑧 ∈ 𝑌)
63		eleq1w 2817	. . . . . . . . . . . . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
70	69	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
71	70	breqd 5107	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 ↔ 𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤))
72		eldifi 4081	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝑋 ∖ 𝑌) → 𝑧 ∈ 𝑋)
73	72	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑧 ∈ 𝑋)
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑧 ∈ 𝑋)
75		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
76		brxp 5671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × 𝑌)𝑤 ↔ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌))
77	74, 75, 76	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑧(𝑋 × 𝑌)𝑤)
78		brin 5148	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ (𝑧(𝑊‘𝑋)𝑤 ∧ 𝑧(𝑋 × 𝑌)𝑤))
79	78	rbaib 538	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × 𝑌)𝑤 → (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
80	77, 79	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
81	71, 80	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
82	1, 2	fpwwe2lem2 10541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑌𝑊𝑅 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
83	82	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑌𝑊𝑅) → ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
84	83	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
85	84	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)))
86	85	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
87	86	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑅 ⊆ (𝑌 × 𝑌))
88	87	ssbrd 5139	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 → 𝑧(𝑌 × 𝑌)𝑤))
89		brxp 5671	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑌 × 𝑌)𝑤 ↔ (𝑧 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌))
90	89	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(𝑌 × 𝑌)𝑤 → 𝑧 ∈ 𝑌)
91	88, 90	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 → 𝑧 ∈ 𝑌))
92	81, 91	sylbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧(𝑊‘𝑋)𝑤 → 𝑧 ∈ 𝑌))
93	68, 92	mtod 198	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑧(𝑊‘𝑋)𝑤)
94	31	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑊‘𝑋) We 𝑋)
95		weso 5613	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑊‘𝑋) Or 𝑋)
97	13	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ 𝑋)
98	97	sselda 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑋)
99		sotric 5560	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑤(𝑊‘𝑋)𝑧 ↔ ¬ (𝑤 = 𝑧 ∨ 𝑧(𝑊‘𝑋)𝑤)))
100		ioran 985	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑤 = 𝑧 ∨ 𝑧(𝑊‘𝑋)𝑤) ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤))
101	99, 100	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑤(𝑊‘𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤)))
102	96, 98, 74, 101	syl12anc 836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑤(𝑊‘𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤)))
103	67, 93, 102	mpbir2and 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤(𝑊‘𝑋)𝑧)
104	103, 44	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}))
105	104	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 ∈ 𝑌 → 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧})))
106	105	ssrdv 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ (◡(𝑊‘𝑋) “ {𝑧}))
107		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)
108	106, 107	eqssd 3949	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 = (◡(𝑊‘𝑋) “ {𝑧}))
109		in32 4180	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌))
110		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
111	110	ineq1d 4169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)))
112	86	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
113		dfss2 3917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ⊆ (𝑌 × 𝑌) ↔ (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
114	112, 113	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
115	111, 114	eqtr3d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = 𝑅)
116		inss2 4188	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑌 × 𝑌)
117		xpss1 5641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 ⊆ 𝑋 → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
118	97, 117	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
119	116, 118	sstrid 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌))
120		dfss2 3917	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌) ↔ (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
121	119, 120	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
122	109, 115, 121	3eqtr3a 2793	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
123	108	sqxpeqd 5654	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) = ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))
124	123	ineq2d 4170	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) = ((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧}))))
125	122, 124	eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧}))))
126	108, 125	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = ((◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))))
127	18	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝐴 ∈ 𝑉)
128	22	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊(𝑊‘𝑋))
129	128	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑋𝑊(𝑊‘𝑋))
130	1, 127, 129	fpwwe2lem3 10542	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑧 ∈ 𝑋) → ((◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))) = 𝑧)
131	73, 130	mpdan 687	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))) = 𝑧)
132	126, 131	eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = 𝑧)
133	132, 62	eqneltrd 2854	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ (𝑌𝐹𝑅) ∈ 𝑌)
134	133	rexlimdvaa 3136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)(◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
135	60, 134	sylbid 240	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
136	37, 135	syld 47	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∖ 𝑌) ≠ ∅ → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
137	136	necon4ad 2949	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑌𝐹𝑅) ∈ 𝑌 → (𝑋 ∖ 𝑌) = ∅))
138	16, 137	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) = ∅)
139		ssdif0 4316	. . . . . . . 8 ⊢ (𝑋 ⊆ 𝑌 ↔ (𝑋 ∖ 𝑌) = ∅)
140	138, 139	sylibr 234	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ⊆ 𝑌)
141	140	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌))) → 𝑋 ⊆ 𝑌))
142	3	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
143		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑊𝑅)
144	1, 17, 142, 128, 143	fpwwe2lem9 10548	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) ∨ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))))
145	15, 141, 144	mpjaod 860	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋 ⊆ 𝑌)
146	13, 145	eqssd 3949	. . . 4 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 = 𝑋)
147	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → Fun 𝑊)
148	146, 143	eqbrtrrd 5120	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊𝑅)
149		funbrfv 6880	. . . . . 6 ⊢ (Fun 𝑊 → (𝑋𝑊𝑅 → (𝑊‘𝑋) = 𝑅))
150	147, 148, 149	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑊‘𝑋) = 𝑅)
151	150	eqcomd 2740	. . . 4 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 = (𝑊‘𝑋))
152	146, 151	jca 511	. . 3 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))
153	152	ex 412	. 2 ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) → (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))
154	1, 2, 3, 4	fpwwe2lem12 10551	. . . 4 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
155	22, 154	jca 511	. . 3 ⊢ (𝜑 → (𝑋𝑊(𝑊‘𝑋) ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
156		breq12 5101	. . . 4 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝑊𝑅 ↔ 𝑋𝑊(𝑊‘𝑋)))
157		oveq12 7365	. . . . 5 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝐹𝑅) = (𝑋𝐹(𝑊‘𝑋)))
158		simpl 482	. . . . 5 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → 𝑌 = 𝑋)
159	157, 158	eleq12d 2828	. . . 4 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → ((𝑌𝐹𝑅) ∈ 𝑌 ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
160	156, 159	anbi12d 632	. . 3 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑋𝑊(𝑊‘𝑋) ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)))
161	155, 160	syl5ibrcom 247	. 2 ⊢ (𝜑 → ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)))
162	153, 161	impbid 212	1 ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  Vcvv 3438  [wsbc 3738   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ∅c0 4283  𝒫 cpw 4552  {csn 4578  ∪ cuni 4861   class class class wbr 5096  {copab 5158   Or wor 5529   Fr wfr 5572   We wwe 5574   × cxp 5620  ^◡ccnv 5621  dom cdm 5622   “ cima 5625  Fun wfun 6484  ‘cfv 6490  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7313  df-ov 7359  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-oi 9413

This theorem is referenced by:  fpwwe  10555  canthwelem  10559  pwfseqlem4  10571