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

Theorem fpwwe2 10057
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 9448. 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 10054 . . . . . . . . . 10 (𝜑𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
65ffund 6511 . . . . . . . . 9 (𝜑 → Fun 𝑊)
7 funbrfv2b 6716 . . . . . . . . 9 (Fun 𝑊 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊𝑌) = 𝑅)))
86, 7syl 17 . . . . . . . 8 (𝜑 → (𝑌𝑊𝑅 ↔ (𝑌 ∈ dom 𝑊 ∧ (𝑊𝑌) = 𝑅)))
98simprbda 501 . . . . . . 7 ((𝜑𝑌𝑊𝑅) → 𝑌 ∈ dom 𝑊)
109adantrr 715 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 ∈ dom 𝑊)
11 elssuni 4859 . . . . . . 7 (𝑌 ∈ dom 𝑊𝑌 dom 𝑊)
1211, 4sseqtrrdi 4016 . . . . . 6 (𝑌 ∈ dom 𝑊𝑌𝑋)
1310, 12syl 17 . . . . 5 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑋)
14 simpl 485 . . . . . . 7 ((𝑋𝑌 ∧ (𝑊𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋𝑌)
1514a1i 11 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋𝑌 ∧ (𝑊𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) → 𝑋𝑌))
16 simplrr 776 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑌𝐹𝑅) ∈ 𝑌)
172adantr 483 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝐴 ∈ V)
1817adantr 483 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝐴 ∈ V)
191, 2, 3, 4fpwwe2lem12 10055 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ dom 𝑊)
20 funfvbrb 6814 . . . . . . . . . . . . . . . . . . . 20 (Fun 𝑊 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
216, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ dom 𝑊𝑋𝑊(𝑊𝑋)))
2219, 21mpbid 234 . . . . . . . . . . . . . . . . . 18 (𝜑𝑋𝑊(𝑊𝑋))
231, 2fpwwe2lem2 10046 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝑊(𝑊𝑋) ↔ ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))))
2422, 23mpbid 234 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
2524ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)) ∧ ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦)))
2625simpld 497 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝐴 ∧ (𝑊𝑋) ⊆ (𝑋 × 𝑋)))
2726simpld 497 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋𝐴)
2818, 27ssexd 5219 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋 ∈ V)
29 difexg 5222 . . . . . . . . . . . . 13 (𝑋 ∈ V → (𝑋𝑌) ∈ V)
3028, 29syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝑌) ∈ V)
3125simprd 498 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊𝑋) We 𝑋 ∧ ∀𝑦𝑋 [((𝑊𝑋) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊𝑋) ∩ (𝑢 × 𝑢))) = 𝑦))
3231simpld 497 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊𝑋) We 𝑋)
33 wefr 5538 . . . . . . . . . . . . 13 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Fr 𝑋)
3432, 33syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊𝑋) Fr 𝑋)
35 difssd 4107 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝑌) ⊆ 𝑋)
36 fri 5510 . . . . . . . . . . . . 13 ((((𝑋𝑌) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ ((𝑋𝑌) ⊆ 𝑋 ∧ (𝑋𝑌) ≠ ∅)) → ∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
3736expr 459 . . . . . . . . . . . 12 ((((𝑋𝑌) ∈ V ∧ (𝑊𝑋) Fr 𝑋) ∧ (𝑋𝑌) ⊆ 𝑋) → ((𝑋𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧))
3830, 34, 35, 37syl21anc 835 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋𝑌) ≠ ∅ → ∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧))
39 ssdif0 4321 . . . . . . . . . . . . . . 15 ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
40 indif1 4246 . . . . . . . . . . . . . . . 16 ((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ∖ 𝑌)
4140eqeq1i 2824 . . . . . . . . . . . . . . 15 (((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ∅ ↔ ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ∖ 𝑌) = ∅)
42 disj 4397 . . . . . . . . . . . . . . . 16 (((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤 ∈ ((𝑊𝑋) “ {𝑧}))
43 vex 3496 . . . . . . . . . . . . . . . . . . . 20 𝑤 ∈ V
4443eliniseg 5951 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V → (𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ 𝑤(𝑊𝑋)𝑧))
4544elv 3498 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ 𝑤(𝑊𝑋)𝑧)
4645notbii 322 . . . . . . . . . . . . . . . . 17 𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ ¬ 𝑤(𝑊𝑋)𝑧)
4746ralbii 3163 . . . . . . . . . . . . . . . 16 (∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤 ∈ ((𝑊𝑋) “ {𝑧}) ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
4842, 47bitri 277 . . . . . . . . . . . . . . 15 (((𝑋𝑌) ∩ ((𝑊𝑋) “ {𝑧})) = ∅ ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
4939, 41, 483bitr2i 301 . . . . . . . . . . . . . 14 ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧)
50 cnvimass 5942 . . . . . . . . . . . . . . . . 17 ((𝑊𝑋) “ {𝑧}) ⊆ dom (𝑊𝑋)
5126simprd 498 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑊𝑋) ⊆ (𝑋 × 𝑋))
52 dmss 5764 . . . . . . . . . . . . . . . . . . 19 ((𝑊𝑋) ⊆ (𝑋 × 𝑋) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
5351, 52syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊𝑋) ⊆ dom (𝑋 × 𝑋))
54 dmxpid 5793 . . . . . . . . . . . . . . . . . 18 dom (𝑋 × 𝑋) = 𝑋
5553, 54sseqtrdi 4015 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → dom (𝑊𝑋) ⊆ 𝑋)
5650, 55sstrid 3976 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑊𝑋) “ {𝑧}) ⊆ 𝑋)
57 sseqin2 4190 . . . . . . . . . . . . . . . 16 (((𝑊𝑋) “ {𝑧}) ⊆ 𝑋 ↔ (𝑋 ∩ ((𝑊𝑋) “ {𝑧})) = ((𝑊𝑋) “ {𝑧}))
5856, 57sylib 220 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋 ∩ ((𝑊𝑋) “ {𝑧})) = ((𝑊𝑋) “ {𝑧}))
5958sseq1d 3996 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋 ∩ ((𝑊𝑋) “ {𝑧})) ⊆ 𝑌 ↔ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌))
6049, 59syl5bbr 287 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧 ↔ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌))
6160rexbidv 3295 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧 ↔ ∃𝑧 ∈ (𝑋𝑌)((𝑊𝑋) “ {𝑧}) ⊆ 𝑌))
62 eldifn 4102 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (𝑋𝑌) → ¬ 𝑧𝑌)
6362ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ 𝑧𝑌)
64 eleq1w 2893 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑌𝑧𝑌))
6564notbid 320 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → (¬ 𝑤𝑌 ↔ ¬ 𝑧𝑌))
6663, 65syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤 = 𝑧 → ¬ 𝑤𝑌))
6766con2d 136 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤𝑌 → ¬ 𝑤 = 𝑧))
6867imp 409 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → ¬ 𝑤 = 𝑧)
6963adantr 483 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → ¬ 𝑧𝑌)
70 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))
7170ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))
7271breqd 5068 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤))
73 eldifi 4101 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝑋𝑌) → 𝑧𝑋)
7473ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑧𝑋)
7574adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑧𝑋)
76 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤𝑌)
77 brxp 5594 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧(𝑋 × 𝑌)𝑤 ↔ (𝑧𝑋𝑤𝑌))
7875, 76, 77sylanbrc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑧(𝑋 × 𝑌)𝑤)
79 brin 5109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤 ↔ (𝑧(𝑊𝑋)𝑤𝑧(𝑋 × 𝑌)𝑤))
8079rbaib 541 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑋 × 𝑌)𝑤 → (𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤𝑧(𝑊𝑋)𝑤))
8178, 80syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧((𝑊𝑋) ∩ (𝑋 × 𝑌))𝑤𝑧(𝑊𝑋)𝑤))
8272, 81bitrd 281 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧(𝑊𝑋)𝑤))
831, 2fpwwe2lem2 10046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑌𝑊𝑅 ↔ ((𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦𝑌 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
8483biimpa 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑌𝑊𝑅) → ((𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦𝑌 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
8584adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)) ∧ (𝑅 We 𝑌 ∧ ∀𝑦𝑌 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
8685simpld 497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌𝐴𝑅 ⊆ (𝑌 × 𝑌)))
8786simprd 498 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
8887ad5ant12 754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑅 ⊆ (𝑌 × 𝑌))
8988ssbrd 5100 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧(𝑌 × 𝑌)𝑤))
90 brxp 5594 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧(𝑌 × 𝑌)𝑤 ↔ (𝑧𝑌𝑤𝑌))
9190simplbi 500 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧(𝑌 × 𝑌)𝑤𝑧𝑌)
9289, 91syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧𝑅𝑤𝑧𝑌))
9382, 92sylbird 262 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑧(𝑊𝑋)𝑤𝑧𝑌))
9469, 93mtod 200 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → ¬ 𝑧(𝑊𝑋)𝑤)
9532ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑊𝑋) We 𝑋)
96 weso 5539 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊𝑋) We 𝑋 → (𝑊𝑋) Or 𝑋)
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑊𝑋) Or 𝑋)
9813ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌𝑋)
9998sselda 3965 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤𝑋)
100 sotric 5494 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊𝑋) Or 𝑋 ∧ (𝑤𝑋𝑧𝑋)) → (𝑤(𝑊𝑋)𝑧 ↔ ¬ (𝑤 = 𝑧𝑧(𝑊𝑋)𝑤)))
101 ioran 979 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (𝑤 = 𝑧𝑧(𝑊𝑋)𝑤) ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊𝑋)𝑤))
102100, 101syl6bb 289 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊𝑋) Or 𝑋 ∧ (𝑤𝑋𝑧𝑋)) → (𝑤(𝑊𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊𝑋)𝑤)))
10397, 99, 75, 102syl12anc 834 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → (𝑤(𝑊𝑋)𝑧 ↔ (¬ 𝑤 = 𝑧 ∧ ¬ 𝑧(𝑊𝑋)𝑤)))
10468, 94, 103mpbir2and 711 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤(𝑊𝑋)𝑧)
105104, 45sylibr 236 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑤𝑌) → 𝑤 ∈ ((𝑊𝑋) “ {𝑧}))
106105ex 415 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑤𝑌𝑤 ∈ ((𝑊𝑋) “ {𝑧})))
107106ssrdv 3971 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 ⊆ ((𝑊𝑋) “ {𝑧}))
108 simprr 771 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)
109107, 108eqssd 3982 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑌 = ((𝑊𝑋) “ {𝑧}))
110 in32 4196 . . . . . . . . . . . . . . . . . 18 (((𝑊𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌))
111 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))
112111ineq1d 4186 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = (((𝑊𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)))
11387ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 ⊆ (𝑌 × 𝑌))
114 df-ss 3950 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ⊆ (𝑌 × 𝑌) ↔ (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
115113, 114sylib 220 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑅 ∩ (𝑌 × 𝑌)) = 𝑅)
116112, 115eqtr3d 2856 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊𝑋) ∩ (𝑋 × 𝑌)) ∩ (𝑌 × 𝑌)) = 𝑅)
117 inss2 4204 . . . . . . . . . . . . . . . . . . . 20 ((𝑊𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑌 × 𝑌)
118 xpss1 5567 . . . . . . . . . . . . . . . . . . . . 21 (𝑌𝑋 → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
11998, 118syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) ⊆ (𝑋 × 𝑌))
120117, 119sstrid 3976 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌))
121 df-ss 3950 . . . . . . . . . . . . . . . . . . 19 (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ⊆ (𝑋 × 𝑌) ↔ (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊𝑋) ∩ (𝑌 × 𝑌)))
122120, 121sylib 220 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊𝑋) ∩ (𝑌 × 𝑌)) ∩ (𝑋 × 𝑌)) = ((𝑊𝑋) ∩ (𝑌 × 𝑌)))
123110, 116, 1223eqtr3a 2878 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊𝑋) ∩ (𝑌 × 𝑌)))
124109sqxpeqd 5580 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌 × 𝑌) = (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))
125124ineq2d 4187 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ((𝑊𝑋) ∩ (𝑌 × 𝑌)) = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧}))))
126123, 125eqtrd 2854 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑅 = ((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧}))))
127109, 126oveq12d 7166 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = (((𝑊𝑋) “ {𝑧})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))))
12818adantr 483 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝐴 ∈ V)
12922adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊(𝑊𝑋))
130129ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → 𝑋𝑊(𝑊𝑋))
1311, 128, 130fpwwe2lem3 10047 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) ∧ 𝑧𝑋) → (((𝑊𝑋) “ {𝑧})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))) = 𝑧)
13274, 131mpdan 685 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (((𝑊𝑋) “ {𝑧})𝐹((𝑊𝑋) ∩ (((𝑊𝑋) “ {𝑧}) × ((𝑊𝑋) “ {𝑧})))) = 𝑧)
133127, 132eqtrd 2854 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → (𝑌𝐹𝑅) = 𝑧)
134133, 63eqneltrd 2930 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) ∧ (𝑧 ∈ (𝑋𝑌) ∧ ((𝑊𝑋) “ {𝑧}) ⊆ 𝑌)) → ¬ (𝑌𝐹𝑅) ∈ 𝑌)
135134rexlimdvaa 3283 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋𝑌)((𝑊𝑋) “ {𝑧}) ⊆ 𝑌 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
13661, 135sylbid 242 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (∃𝑧 ∈ (𝑋𝑌)∀𝑤 ∈ (𝑋𝑌) ¬ 𝑤(𝑊𝑋)𝑧 → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
13738, 136syld 47 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑋𝑌) ≠ ∅ → ¬ (𝑌𝐹𝑅) ∈ 𝑌))
138137necon4ad 3033 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → ((𝑌𝐹𝑅) ∈ 𝑌 → (𝑋𝑌) = ∅))
13916, 138mpd 15 . . . . . . . 8 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → (𝑋𝑌) = ∅)
140 ssdif0 4321 . . . . . . . 8 (𝑋𝑌 ↔ (𝑋𝑌) = ∅)
141139, 140sylibr 236 . . . . . . 7 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))) → 𝑋𝑌)
142141ex 415 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌))) → 𝑋𝑌))
1433adantlr 713 . . . . . . 7 (((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
144 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌𝑊𝑅)
1451, 17, 143, 129, 144fpwwe2lem10 10053 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → ((𝑋𝑌 ∧ (𝑊𝑋) = (𝑅 ∩ (𝑌 × 𝑋))) ∨ (𝑌𝑋𝑅 = ((𝑊𝑋) ∩ (𝑋 × 𝑌)))))
14615, 142, 145mpjaod 856 . . . . 5 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑌)
14713, 146eqssd 3982 . . . 4 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑌 = 𝑋)
1486adantr 483 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → Fun 𝑊)
149147, 144eqbrtrrd 5081 . . . . . 6 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑋𝑊𝑅)
150 funbrfv 6709 . . . . . 6 (Fun 𝑊 → (𝑋𝑊𝑅 → (𝑊𝑋) = 𝑅))
151148, 149, 150sylc 65 . . . . 5 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑊𝑋) = 𝑅)
152151eqcomd 2825 . . . 4 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → 𝑅 = (𝑊𝑋))
153147, 152jca 514 . . 3 ((𝜑 ∧ (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)) → (𝑌 = 𝑋𝑅 = (𝑊𝑋)))
154153ex 415 . 2 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) → (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
1551, 2, 3, 4fpwwe2lem13 10056 . . . 4 (𝜑 → (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)
15622, 155jca 514 . . 3 (𝜑 → (𝑋𝑊(𝑊𝑋) ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
157 breq12 5062 . . . 4 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → (𝑌𝑊𝑅𝑋𝑊(𝑊𝑋)))
158 oveq12 7157 . . . . 5 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → (𝑌𝐹𝑅) = (𝑋𝐹(𝑊𝑋)))
159 simpl 485 . . . . 5 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → 𝑌 = 𝑋)
160158, 159eleq12d 2905 . . . 4 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → ((𝑌𝐹𝑅) ∈ 𝑌 ↔ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋))
161157, 160anbi12d 632 . . 3 ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑋𝑊(𝑊𝑋) ∧ (𝑋𝐹(𝑊𝑋)) ∈ 𝑋)))
162156, 161syl5ibrcom 249 . 2 (𝜑 → ((𝑌 = 𝑋𝑅 = (𝑊𝑋)) → (𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌)))
163154, 162impbid 214 1 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1081   = wceq 1530  wcel 2107  wne 3014  wral 3136  wrex 3137  Vcvv 3493  [wsbc 3770  cdif 3931  cin 3933  wss 3934  c0 4289  𝒫 cpw 4537  {csn 4559   cuni 4830   class class class wbr 5057  {copab 5119   Or wor 5466   Fr wfr 5504   We wwe 5506   × cxp 5546  ccnv 5547  dom cdm 5548  cima 5551  Fun wfun 6342  cfv 6348  (class class class)co 7148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-wrecs 7939  df-recs 8000  df-oi 8966
This theorem is referenced by:  fpwwe  10060  canthwelem  10064  pwfseqlem4  10076
  Copyright terms: Public domain W3C validator