Theorem fpwwe2 10579

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 9966. 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 10576	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
6	5	ffund 6672	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝑊)
7		funbrfv2b 6900	. . . . . . . . 9 ⊢ (Fun 𝑊 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊‘𝑌) = 𝑅)))
8	6, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊‘𝑌) = 𝑅)))
9	8	simprbda 499	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌𝑊𝑅) → 𝑌 ∈ dom 𝑊)
10	9	adantrr 715	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ∈ dom 𝑊)
11		elssuni 4898	. . . . . . 7 ⊢ (𝑌 ∈ dom 𝑊 → 𝑌 ⊆ ∪ dom 𝑊)
12	11, 4	sseqtrrdi 3995	. . . . . 6 ⊢ (𝑌 ∈ dom 𝑊 → 𝑌 ⊆ 𝑋)
13	10, 12	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ⊆ 𝑋)
14		simpl 483	. . . . . . 7 ⊢ ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋 ⊆ 𝑌)
15	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋 ⊆ 𝑌))
16		simplrr 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑌𝐹𝑅) ∈ 𝑌)
17	2	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝐴 ∈ 𝑉)
18	17	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝐴 ∈ 𝑉)
19	1, 2, 3, 4	fpwwe2lem11 10577	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)
20		funfvbrb 7001	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝑊 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
21	6, 20	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋 ∈ dom 𝑊 ↔ 𝑋𝑊(𝑊‘𝑋)))
22	19, 21	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋𝑊(𝑊‘𝑋))
23	1, 2	fpwwe2lem2 10568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝑊(𝑊‘𝑋) ↔ ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
24	22, 23	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
25	24	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
26	25	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ⊆ 𝐴 ∧ (𝑊‘𝑋) ⊆ (𝑋 × 𝑋)))
27	26	simpld 495	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ⊆ 𝐴)
28	18, 27	ssexd 5281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ∈ V)
29	28	difexd 5286	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) ∈ V)
30	25	simprd 496	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊‘𝑋) We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡(𝑊‘𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
31	30	simpld 495	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) We 𝑋)
32		wefr 5623	. . . . . . . . . . . . 13 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Fr 𝑋)
33	31, 32	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) Fr 𝑋)
34		difssd 4092	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) ⊆ 𝑋)
35		fri 5593	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∖ 𝑌) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ ((𝑋 ∖ 𝑌) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑌) ≠ ∅)) → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
36	35	expr 457	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∖ 𝑌) ∈ V ∧ (𝑊‘𝑋) Fr 𝑋) ∧ (𝑋 ∖ 𝑌) ⊆ 𝑋) → ((𝑋 ∖ 𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧))
37	29, 33, 34, 36	syl21anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∖ 𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧))
38		ssdif0 4323	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
39		indif1 4231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌)
40	39	eqeq1i 2741	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
41		disj 4407	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}))
42		vex 3449	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑤 ∈ V
43	42	eliniseg 6046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ V → (𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ 𝑤(𝑊‘𝑋)𝑧))
44	43	elv 3451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ 𝑤(𝑊‘𝑋)𝑧)
45	44	notbii 319	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ ¬ 𝑤(𝑊‘𝑋)𝑧)
46	45	ralbii 3096	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}) ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
47	41, 46	bitri 274	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑌) ∩ (◡(𝑊‘𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
48	38, 40, 47	3bitr2i 298	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧)
49		cnvimass 6033	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ dom (𝑊‘𝑋)
50	26	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊‘𝑋) ⊆ (𝑋 × 𝑋))
51		dmss 5858	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊‘𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊‘𝑋) ⊆ dom (𝑋 × 𝑋))
53		dmxpid 5885	. . . . . . . . . . . . . . . . . 18 ⊢ dom (𝑋 × 𝑋) = 𝑋
54	52, 53	sseqtrdi 3994	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊‘𝑋) ⊆ 𝑋)
55	49, 54	sstrid 3955	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑋)
56		sseqin2 4175	. . . . . . . . . . . . . . . 16 ⊢ ((◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑋 ↔ (𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) = (◡(𝑊‘𝑋) “ {𝑧}))
57	55, 56	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) = (◡(𝑊‘𝑋) “ {𝑧}))
58	57	sseq1d 3975	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∩ (◡(𝑊‘𝑋) “ {𝑧})) ⊆ 𝑌 ↔ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
59	48, 58	bitr3id 284	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 ↔ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
60	59	rexbidv 3175	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 ↔ ∃𝑧 ∈ (𝑋 ∖ 𝑌)(◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌))
61		eldifn 4087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (𝑋 ∖ 𝑌) → ¬ 𝑧 ∈ 𝑌)
62	61	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ 𝑧 ∈ 𝑌)
63		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑌 ↔ 𝑧 ∈ 𝑌))
64	63	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑧 → (¬ 𝑤 ∈ 𝑌 ↔ ¬ 𝑧 ∈ 𝑌))
65	62, 64	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 = 𝑧 → ¬ 𝑤 ∈ 𝑌))
66	65	con2d 134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 ∈ 𝑌 → ¬ 𝑤 = 𝑧))
67	66	imp 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑤 = 𝑧)
68	62	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑧 ∈ 𝑌)
69		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
70	69	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
71	70	breqd 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 ↔ 𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤))
72		eldifi 4086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝑋 ∖ 𝑌) → 𝑧 ∈ 𝑋)
73	72	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑧 ∈ 𝑋)
74	73	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑧 ∈ 𝑋)
75		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌)
76		brxp 5681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧(𝑋 × 𝑌)𝑤 ↔ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌))
77	74, 75, 76	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑧(𝑋 × 𝑌)𝑤)
78		brin 5157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ (𝑧(𝑊‘𝑋)𝑤 ∧ 𝑧(𝑋 × 𝑌)𝑤))
79	78	rbaib 539	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑋 × 𝑌)𝑤 → (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
80	77, 79	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧((𝑊‘𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
81	71, 80	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 ↔ 𝑧(𝑊‘𝑋)𝑤))
82	1, 2	fpwwe2lem2 10568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝑌𝑊𝑅 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
83	82	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑌𝑊𝑅) → ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
84	83	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
85	84	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑌 × 𝑌)))
86	85	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
87	86	ad5ant12 754	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑅 ⊆ (𝑌 × 𝑌))
88	87	ssbrd 5148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 → 𝑧(𝑌 × 𝑌)𝑤))
89		brxp 5681	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧(𝑌 × 𝑌)𝑤 ↔ (𝑧 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌))
90	89	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧(𝑌 × 𝑌)𝑤 → 𝑧 ∈ 𝑌)
91	88, 90	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧𝑅𝑤 → 𝑧 ∈ 𝑌))
92	81, 91	sylbird 259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑧(𝑊‘𝑋)𝑤 → 𝑧 ∈ 𝑌))
93	68, 92	mtod 197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → ¬ 𝑧(𝑊‘𝑋)𝑤)
94	31	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑊‘𝑋) We 𝑋)
95		weso 5624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊‘𝑋) We 𝑋 → (𝑊‘𝑋) Or 𝑋)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑊‘𝑋) Or 𝑋)
97	13	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ 𝑋)
98	97	sselda 3944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑋)
99		sotric 5573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑤(𝑊‘𝑋)𝑧 ↔ ¬ (𝑤 = 𝑧 ∨ 𝑧(𝑊‘𝑋)𝑤)))
100		ioran 982	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑤 = 𝑧 ∨ 𝑧(𝑊‘𝑋)𝑤) ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤))
101	99, 100	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊‘𝑋) Or 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑤(𝑊‘𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤)))
102	96, 98, 74, 101	syl12anc 835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → (𝑤(𝑊‘𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊‘𝑋)𝑤)))
103	67, 93, 102	mpbir2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤(𝑊‘𝑋)𝑧)
104	103, 44	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧}))
105	104	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 ∈ 𝑌 → 𝑤 ∈ (◡(𝑊‘𝑋) “ {𝑧})))
106	105	ssrdv 3950	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ (◡(𝑊‘𝑋) “ {𝑧}))
107		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)
108	106, 107	eqssd 3961	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 = (◡(𝑊‘𝑋) “ {𝑧}))
109		in32 4181	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌))
110		simplrr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))
111	110	ineq1d 4171	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)))
112	86	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
113		df-ss 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ⊆ (𝑌 × 𝑌) ↔ (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
114	112, 113	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
115	111, 114	eqtr3d 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊‘𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = 𝑅)
116		inss2 4189	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑌 × 𝑌)
117		xpss1 5652	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 ⊆ 𝑋 → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
118	97, 117	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
119	116, 118	sstrid 3955	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌))
120		df-ss 3927	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌) ↔ (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
121	119, 120	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
122	109, 115, 121	3eqtr3a 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)))
123	108	sqxpeqd 5665	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) = ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))
124	123	ineq2d 4172	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊‘𝑋) ∩ (𝑌 × 𝑌)) = ((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧}))))
125	122, 124	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧}))))
126	108, 125	oveq12d 7375	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = ((◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))))
127	18	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝐴 ∈ 𝑉)
128	22	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊(𝑊‘𝑋))
129	128	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑋𝑊(𝑊‘𝑋))
130	1, 127, 129	fpwwe2lem3 10569	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑧 ∈ 𝑋) → ((◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))) = 𝑧)
131	73, 130	mpdan 685	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ((◡(𝑊‘𝑋) “ {𝑧})𝐹((𝑊‘𝑋) ∩ ((◡(𝑊‘𝑋) “ {𝑧}) × (◡(𝑊‘𝑋) “ {𝑧})))) = 𝑧)
132	126, 131	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = 𝑧)
133	132, 62	eqneltrd 2857	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋 ∖ 𝑌) ∧ (◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ (𝑌𝐹𝑅) ∈ 𝑌)
134	133	rexlimdvaa 3153	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)(◡(𝑊‘𝑋) “ {𝑧}) ⊆ 𝑌 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
135	60, 134	sylbid 239	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋 ∖ 𝑌)∀𝑤 ∈ (𝑋 ∖ 𝑌) ¬ 𝑤(𝑊‘𝑋)𝑧 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
136	37, 135	syld 47	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∖ 𝑌) ≠ ∅ → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
137	136	necon4ad 2962	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑌𝐹𝑅) ∈ 𝑌 → (𝑋 ∖ 𝑌) = ∅))
138	16, 137	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∖ 𝑌) = ∅)
139		ssdif0 4323	. . . . . . . 8 ⊢ (𝑋 ⊆ 𝑌 ↔ (𝑋 ∖ 𝑌) = ∅)
140	138, 139	sylibr 233	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ⊆ 𝑌)
141	140	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌))) → 𝑋 ⊆ 𝑌))
142	3	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
143		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑊𝑅)
144	1, 17, 142, 128, 143	fpwwe2lem9 10575	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋 ⊆ 𝑌 ∧ (𝑊‘𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) ∨ (𝑌 ⊆ 𝑋 ∧ 𝑅 = ((𝑊‘𝑋) ∩ (𝑋 × 𝑌)))))
145	15, 141, 144	mpjaod 858	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋 ⊆ 𝑌)
146	13, 145	eqssd 3961	. . . 4 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 = 𝑋)
147	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → Fun 𝑊)
148	146, 143	eqbrtrrd 5129	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊𝑅)
149		funbrfv 6893	. . . . . 6 ⊢ (Fun 𝑊 → (𝑋𝑊𝑅 → (𝑊‘𝑋) = 𝑅))
150	147, 148, 149	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑊‘𝑋) = 𝑅)
151	150	eqcomd 2742	. . . 4 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 = (𝑊‘𝑋))
152	146, 151	jca 512	. . 3 ⊢ ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))
153	152	ex 413	. 2 ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) → (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))
154	1, 2, 3, 4	fpwwe2lem12 10578	. . . 4 ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
155	22, 154	jca 512	. . 3 ⊢ (𝜑 → (𝑋𝑊(𝑊‘𝑋) ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
156		breq12 5110	. . . 4 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝑊𝑅 ↔ 𝑋𝑊(𝑊‘𝑋)))
157		oveq12 7366	. . . . 5 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝐹𝑅) = (𝑋𝐹(𝑊‘𝑋)))
158		simpl 483	. . . . 5 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → 𝑌 = 𝑋)
159	157, 158	eleq12d 2832	. . . 4 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → ((𝑌𝐹𝑅) ∈ 𝑌 ↔ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋))
160	156, 159	anbi12d 631	. . 3 ⊢ ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑋𝑊(𝑊‘𝑋) ∧ (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)))
161	155, 160	syl5ibrcom 246	. 2 ⊢ (𝜑 → ((𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)) → (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)))
162	153, 161	impbid 211	1 ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  Vcvv 3445  [wsbc 3739   ∖ cdif 3907   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865   class class class wbr 5105  {copab 5167   Or wor 5544   Fr wfr 5585   We wwe 5587   × cxp 5631  ^◡ccnv 5632  dom cdm 5633   “ cima 5636  Fun wfun 6490  ‘cfv 6496  (class class class)co 7357

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-oi 9446

This theorem is referenced by:  fpwwe  10582  canthwelem  10586  pwfseqlem4  10598