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

Theorem fpwwe2 9780
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 9166. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
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.
StepHypRef Expression
1 fpwwe2.1 . . . . . . . . . . 11 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
2 fpwwe2.2 . . . . . . . . . . 11 (𝜑𝐴 ∈ V)
3 fpwwe2.3 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
4 fpwwe2.4 . . . . . . . . . . 11 𝑋 = dom 𝑊
51, 2, 3, 4fpwwe2lem11 9777 . . . . . . . . . 10 (𝜑𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
65ffund 6282 . . . . . . . . 9 (𝜑 → Fun 𝑊)
7 funbrfv2b 6487 . . . . . . . . 9 (Fun 𝑊 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊𝑌) = 𝑅)))
86, 7syl 17 . . . . . . . 8 (𝜑 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊𝑌) = 𝑅)))
98simprbda 494 . . . . . . 7 ((𝜑𝑌𝑊𝑅) → 𝑌 ∈ dom 𝑊)
109adantrr 710 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ∈ dom 𝑊)
11 elssuni 4689 . . . . . . 7 (𝑌 ∈ dom 𝑊𝑌 dom 𝑊)
1211, 4syl6sseqr 3877 . . . . . 6 (𝑌 ∈ dom 𝑊𝑌𝑋)
1310, 12syl 17 . . . . 5 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑋)
14 simpl 476 . . . . . . 7 ((𝑋𝑌 ∧ (𝑊𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋𝑌)
1514a1i 11 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋𝑌 ∧ (𝑊𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋𝑌))
16 simplrr 798 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑌𝐹𝑅) ∈ 𝑌)
172adantr 474 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝐴 ∈ V)
1817adantr 474 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝐴 ∈ V)
191, 2, 3, 4fpwwe2lem12 9778 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ dom 𝑊)
20 funfvbrb 6579 . . . . . . . . . . . . . . . . . . . 20 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
216, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
2219, 21mpbid 224 . . . . . . . . . . . . . . . . . 18 (𝜑𝑋𝑊(𝑊𝑋))
231, 2fpwwe2lem2 9769 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
2422, 23mpbid 224 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
2524ad2antrr 719 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
2625simpld 490 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
2726simpld 490 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋𝐴)
2818, 27ssexd 5030 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ∈ V)
29 difexg 5033 . . . . . . . . . . . . 13 (𝑋 ∈ V → (𝑋𝑌) ∈ V)
3028, 29syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝑌) ∈ V)
3125simprd 491 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
3231simpld 490 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊𝑋) We 𝑋)
33 wefr 5332 . . . . . . . . . . . . 13 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
3432, 33syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊𝑋) Fr 𝑋)
35 difssd 3965 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝑌) ⊆ 𝑋)
36 fri 5304 . . . . . . . . . . . . 13 ((((𝑋𝑌) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑋𝑌) ⊆ 𝑋 ∧ (𝑋𝑌) ≠ ∅)) → ∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
3736expr 450 . . . . . . . . . . . 12 ((((𝑋𝑌) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ (𝑋𝑌) ⊆ 𝑋) → ((𝑋𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧))
3830, 34, 35, 37syl21anc 873 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧))
39 ssdif0 4171 . . . . . . . . . . . . . . 15 ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
40 indif1 4101 . . . . . . . . . . . . . . . 16 ((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ∖ 𝑌)
4140eqeq1i 2830 . . . . . . . . . . . . . . 15 (((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ∅ ↔ ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
42 disj 4241 . . . . . . . . . . . . . . . 16 (((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤 ∈ ((𝑊𝑋) “ {𝑧}))
43 vex 3417 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
44 vex 3417 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ V
4544eliniseg 5735 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V → (𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ 𝑤(𝑊𝑋)𝑧))
4643, 45ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ 𝑤(𝑊𝑋)𝑧)
4746notbii 312 . . . . . . . . . . . . . . . . 17 𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ ¬ 𝑤(𝑊𝑋)𝑧)
4847ralbii 3189 . . . . . . . . . . . . . . . 16 (∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
4942, 48bitri 267 . . . . . . . . . . . . . . 15 (((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
5039, 41, 493bitr2i 291 . . . . . . . . . . . . . 14 ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
51 cnvimass 5726 . . . . . . . . . . . . . . . . 17 ((𝑊𝑋) “ {𝑧}) ⊆ dom (𝑊𝑋)
5226simprd 491 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
53 dmss 5555 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
5452, 53syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
55 dmxpid 5577 . . . . . . . . . . . . . . . . . 18 dom (𝑋 × 𝑋) = 𝑋
5654, 55syl6sseq 3876 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊𝑋) ⊆ 𝑋)
5751, 56syl5ss 3838 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊𝑋) “ {𝑧}) ⊆ 𝑋)
58 sseqin2 4044 . . . . . . . . . . . . . . . 16 (((𝑊𝑋) “ {𝑧}) ⊆ 𝑋 ↔ (𝑋 ∩ ((𝑊𝑋) “ {𝑧})) = ((𝑊𝑋) “ {𝑧}))
5957, 58sylib 210 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∩ ((𝑊𝑋) “ {𝑧})) = ((𝑊𝑋) “ {𝑧}))
6059sseq1d 3857 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌))
6150, 60syl5bbr 277 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧 ↔ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌))
6261rexbidv 3262 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧 ↔ ∃𝑧 ∈ (𝑋𝑌)((𝑊𝑋) “ {𝑧}) ⊆ 𝑌))
63 eldifn 3960 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (𝑋𝑌) → ¬ 𝑧𝑌)
6463ad2antrl 721 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ 𝑧𝑌)
65 eleq1w 2889 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑌𝑧𝑌))
6665notbid 310 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → (¬ 𝑤𝑌 ↔ ¬ 𝑧𝑌))
6764, 66syl5ibrcom 239 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 = 𝑧 → ¬ 𝑤𝑌))
6867con2d 132 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤𝑌 → ¬ 𝑤 = 𝑧))
6968imp 397 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → ¬ 𝑤 = 𝑧)
7064adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → ¬ 𝑧𝑌)
71 simprr 791 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))
7271ad2antrr 719 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))
7372breqd 4884 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤))
74 eldifi 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝑋𝑌) → 𝑧𝑋)
7574ad2antrl 721 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑧𝑋)
7675adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑧𝑋)
77 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤𝑌)
78 brxp 5388 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × 𝑌)𝑤 ↔ (𝑧𝑋𝑤𝑌))
7976, 77, 78sylanbrc 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑧(𝑋 × 𝑌)𝑤)
80 brin 4925 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ (𝑧(𝑊𝑋)𝑤𝑧(𝑋 × 𝑌)𝑤))
8180rbaib 536 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × 𝑌)𝑤 → (𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤𝑧(𝑊𝑋)𝑤))
8279, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤𝑧(𝑊𝑋)𝑤))
8373, 82bitrd 271 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧(𝑊𝑋)𝑤))
841, 2fpwwe2lem2 9769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑌𝑊𝑅 ↔ ((𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦𝑌 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
8584biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑌𝑊𝑅) → ((𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦𝑌 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
8685adantrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦𝑌 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
8786simpld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)))
8887simprd 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
8988ad3antrrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑅 ⊆ (𝑌 × 𝑌))
9089ssbrd 4916 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧(𝑌 × 𝑌)𝑤))
91 brxp 5388 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑌 × 𝑌)𝑤 ↔ (𝑧𝑌𝑤𝑌))
9291simplbi 493 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(𝑌 × 𝑌)𝑤𝑧𝑌)
9390, 92syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧𝑌))
9483, 93sylbird 252 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧(𝑊𝑋)𝑤𝑧𝑌))
9570, 94mtod 190 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → ¬ 𝑧(𝑊𝑋)𝑤)
9632ad2antrr 719 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑊𝑋) We 𝑋)
97 weso 5333 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
9896, 97syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑊𝑋) Or 𝑋)
9913ad2antrr 719 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌𝑋)
10099sselda 3827 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤𝑋)
101 sotric 5289 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊𝑋) Or 𝑋 ∧ (𝑤𝑋𝑧𝑋)) → (𝑤(𝑊𝑋)𝑧 ↔ ¬ (𝑤 = 𝑧𝑧(𝑊𝑋)𝑤)))
102 ioran 1013 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (𝑤 = 𝑧𝑧(𝑊𝑋)𝑤) ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊𝑋)𝑤))
103101, 102syl6bb 279 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊𝑋) Or 𝑋 ∧ (𝑤𝑋𝑧𝑋)) → (𝑤(𝑊𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊𝑋)𝑤)))
10498, 100, 76, 103syl12anc 872 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑤(𝑊𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊𝑋)𝑤)))
10569, 95, 104mpbir2and 706 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤(𝑊𝑋)𝑧)
106105, 46sylibr 226 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤 ∈ ((𝑊𝑋) “ {𝑧}))
107106ex 403 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤𝑌𝑤 ∈ ((𝑊𝑋) “ {𝑧})))
108107ssrdv 3833 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ ((𝑊𝑋) “ {𝑧}))
109 simprr 791 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)
110108, 109eqssd 3844 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 = ((𝑊𝑋) “ {𝑧}))
111 in32 4050 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌))
112 simplrr 798 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))
113112ineq1d 4040 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = (((𝑊𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)))
11488ad2antrr 719 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
115 df-ss 3812 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ⊆ (𝑌 × 𝑌) ↔ (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
116114, 115sylib 210 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
117113, 116eqtr3d 2863 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = 𝑅)
118 inss2 4058 . . . . . . . . . . . . . . . . . . . 20 ((𝑊𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑌 × 𝑌)
119 xpss1 5361 . . . . . . . . . . . . . . . . . . . . 21 (𝑌𝑋 → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
12099, 119syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
121118, 120syl5ss 3838 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌))
122 df-ss 3812 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌) ↔ (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊𝑋) ∩ (𝑌 × 𝑌)))
123121, 122sylib 210 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊𝑋) ∩ (𝑌 × 𝑌)))
124111, 117, 1233eqtr3a 2885 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊𝑋) ∩ (𝑌 × 𝑌)))
125110sqxpeqd 5374 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) = (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))
126125ineq2d 4041 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊𝑋) ∩ (𝑌 × 𝑌)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧}))))
127124, 126eqtrd 2861 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧}))))
128110, 127oveq12d 6923 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = (((𝑊𝑋) “ {𝑧})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))))
12918adantr 474 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝐴 ∈ V)
13022adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊(𝑊𝑋))
131130ad2antrr 719 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑋𝑊(𝑊𝑋))
1321, 129, 131fpwwe2lem3 9770 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑧𝑋) → (((𝑊𝑋) “ {𝑧})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))) = 𝑧)
13375, 132mpdan 680 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊𝑋) “ {𝑧})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))) = 𝑧)
134128, 133eqtrd 2861 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = 𝑧)
135134, 64eqneltrd 2925 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ (𝑌𝐹𝑅) ∈ 𝑌)
136135rexlimdvaa 3241 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋𝑌)((𝑊𝑋) “ {𝑧}) ⊆ 𝑌 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
13762, 136sylbid 232 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
13838, 137syld 47 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋𝑌) ≠ ∅ → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
139138necon4ad 3018 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑌𝐹𝑅) ∈ 𝑌 → (𝑋𝑌) = ∅))
14016, 139mpd 15 . . . . . . . 8 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝑌) = ∅)
141 ssdif0 4171 . . . . . . . 8 (𝑋𝑌 ↔ (𝑋𝑌) = ∅)
142140, 141sylibr 226 . . . . . . 7 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋𝑌)
143142ex 403 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌))) → 𝑋𝑌))
1443adantlr 708 . . . . . . 7 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
145 simprl 789 . . . . . . 7 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑊𝑅)
1461, 17, 144, 130, 145fpwwe2lem10 9776 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋𝑌 ∧ (𝑊𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) ∨ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))))
14715, 143, 146mpjaod 893 . . . . 5 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑌)
14813, 147eqssd 3844 . . . 4 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 = 𝑋)
1496adantr 474 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → Fun 𝑊)
150148, 145eqbrtrrd 4897 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊𝑅)
151 funbrfv 6480 . . . . . 6 (Fun 𝑊 → (𝑋𝑊𝑅 → (𝑊𝑋) = 𝑅))
152149, 150, 151sylc 65 . . . . 5 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑊𝑋) = 𝑅)
153152eqcomd 2831 . . . 4 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 = (𝑊𝑋))
154148, 153jca 509 . . 3 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 = 𝑋𝑅 = (𝑊𝑋)))
155154ex 403 . 2 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) → (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
1561, 2, 3, 4fpwwe2lem13 9779 . . . 4 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
15722, 156jca 509 . . 3 (𝜑 → (𝑋𝑊(𝑊𝑋) ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
158 breq12 4878 . . . 4 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → (𝑌𝑊𝑅𝑋𝑊(𝑊𝑋)))
159 oveq12 6914 . . . . 5 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → (𝑌𝐹𝑅) = (𝑋𝐹(𝑊𝑋)))
160 simpl 476 . . . . 5 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → 𝑌 = 𝑋)
161159, 160eleq12d 2900 . . . 4 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → ((𝑌𝐹𝑅) ∈ 𝑌 ↔ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
162158, 161anbi12d 626 . . 3 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑋𝑊(𝑊𝑋) ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)))
163157, 162syl5ibrcom 239 . 2 (𝜑 → ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)))
164155, 163impbid 204 1 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 880  w3a 1113   = wceq 1658  wcel 2166  wne 2999  wral 3117  wrex 3118  Vcvv 3414  [wsbc 3662  cdif 3795  cin 3797  wss 3798  c0 4144  𝒫 cpw 4378  {csn 4397   cuni 4658   class class class wbr 4873  {copab 4935   Or wor 5262   Fr wfr 5298   We wwe 5300   × cxp 5340  ccnv 5341  dom cdm 5342  cima 5345  Fun wfun 6117  cfv 6123  (class class class)co 6905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-wrecs 7672  df-recs 7734  df-oi 8684
This theorem is referenced by:  fpwwe  9783  canthwelem  9787  pwfseqlem4  9799
  Copyright terms: Public domain W3C validator