Metamath Proof Explorer

Theorem fpwwe2

Description: Given any function F from well-orderings of subsets of A to A , there is a unique well-ordered subset <. X , ( WX ) >. which "agrees" with F 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 . Theorem 1.1 of KanamoriPincus p. 415. (Contributed by Mario Carneiro, 18-May-2015) (Revised by AV, 20-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2.4 ⊢ 𝑋 = ∪ dom 𝑊
5 1 2 3 4 fpwwe2lem10 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 ⟶ 𝒫 ( 𝑋 × 𝑋 ) )
6 5 ffund ⊢ ( 𝜑 → Fun 𝑊 )
7 funbrfv2b ⊢ ( Fun 𝑊 → ( 𝑌 𝑊 𝑅 ↔ ( 𝑌 ∈ dom 𝑊 ∧ ( 𝑊 ‘ 𝑌 ) = 𝑅 ) ) )
8 6 7 syl ⊢ ( 𝜑 → ( 𝑌 𝑊 𝑅 ↔ ( 𝑌 ∈ dom 𝑊 ∧ ( 𝑊 ‘ 𝑌 ) = 𝑅 ) ) )
9 8 simprbda ⊢ ( ( 𝜑 ∧ 𝑌 𝑊 𝑅 ) → 𝑌 ∈ dom 𝑊 )
10 9 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑌 ∈ dom 𝑊 )
11 elssuni ⊢ ( 𝑌 ∈ dom 𝑊 → 𝑌 ⊆ ∪ dom 𝑊 )
12 11 4 sseqtrrdi ⊢ ( 𝑌 ∈ dom 𝑊 → 𝑌 ⊆ 𝑋 )
13 10 12 syl ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
14 simpl ⊢ ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑊 ‘ 𝑋 ) = ( 𝑅 ∩ ( 𝑌 × 𝑋 ) ) ) → 𝑋 ⊆ 𝑌 )
15 14 a1i ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑊 ‘ 𝑋 ) = ( 𝑅 ∩ ( 𝑌 × 𝑋 ) ) ) → 𝑋 ⊆ 𝑌 ) )
16 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 )
17 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝐴 ∈ 𝑉 )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → 𝐴 ∈ 𝑉 )
19 1 2 3 4 fpwwe2lem11 ⊢ ( 𝜑 → 𝑋 ∈ dom 𝑊 )
20 funfvbrb ⊢ ( Fun 𝑊 → ( 𝑋 ∈ dom 𝑊 ↔ 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ) )
21 6 20 syl ⊢ ( 𝜑 → ( 𝑋 ∈ dom 𝑊 ↔ 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ) )
22 19 21 mpbid ⊢ ( 𝜑 → 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) )
23 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ↔ ( ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
24 22 23 mpbid ⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
26 25 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) )
27 26 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → 𝑋 ⊆ 𝐴 )
28 18 27 ssexd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → 𝑋 ∈ V )
29 28 difexd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑋 ∖ 𝑌 ) ∈ V )
30 25 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
31 30 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑊 ‘ 𝑋 ) We 𝑋 )
32 wefr ⊢ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 → ( 𝑊 ‘ 𝑋 ) Fr 𝑋 )
33 31 32 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑊 ‘ 𝑋 ) Fr 𝑋 )
34 difssd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑋 ∖ 𝑌 ) ⊆ 𝑋 )
35 fri ⊢ ( ( ( ( 𝑋 ∖ 𝑌 ) ∈ V ∧ ( 𝑊 ‘ 𝑋 ) Fr 𝑋 ) ∧ ( ( 𝑋 ∖ 𝑌 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑌 ) ≠ ∅ ) ) → ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
36 35 expr ⊢ ( ( ( ( 𝑋 ∖ 𝑌 ) ∈ V ∧ ( 𝑊 ‘ 𝑋 ) Fr 𝑋 ) ∧ ( 𝑋 ∖ 𝑌 ) ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑌 ) ≠ ∅ → ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ) )
37 29 33 34 36 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑋 ∖ 𝑌 ) ≠ ∅ → ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ) )
38 ssdif0 ⊢ ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ⊆ 𝑌 ↔ ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ∖ 𝑌 ) = ∅ )
39 indif1 ⊢ ( ( 𝑋 ∖ 𝑌 ) ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) = ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ∖ 𝑌 )
40 39 eqeq1i ⊢ ( ( ( 𝑋 ∖ 𝑌 ) ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) = ∅ ↔ ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ∖ 𝑌 ) = ∅ )
41 disj ⊢ ( ( ( 𝑋 ∖ 𝑌 ) ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) = ∅ ↔ ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) )
42 vex ⊢ 𝑤 ∈ V
43 42 eliniseg ⊢ ( 𝑧 ∈ V → ( 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ↔ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ) )
44 43 elv ⊢ ( 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ↔ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
45 44 notbii ⊢ ( ¬ 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ↔ ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
46 45 ralbii ⊢ ( ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ↔ ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
47 41 46 bitri ⊢ ( ( ( 𝑋 ∖ 𝑌 ) ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) = ∅ ↔ ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
48 38 40 47 3bitr2i ⊢ ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ⊆ 𝑌 ↔ ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
49 cnvimass ⊢ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ dom ( 𝑊 ‘ 𝑋 )
50 26 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) )
51 dmss ⊢ ( ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) → dom ( 𝑊 ‘ 𝑋 ) ⊆ dom ( 𝑋 × 𝑋 ) )
52 50 51 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → dom ( 𝑊 ‘ 𝑋 ) ⊆ dom ( 𝑋 × 𝑋 ) )
53 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
54 52 53 sseqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → dom ( 𝑊 ‘ 𝑋 ) ⊆ 𝑋 )
55 49 54 sstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑋 )
56 sseqin2 ⊢ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑋 ↔ ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) = ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) )
57 55 56 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) = ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) )
58 57 sseq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ⊆ 𝑌 ↔ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) )
59 48 58 bitr3id ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ↔ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) )
60 59 rexbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ↔ ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) )
61 eldifn ⊢ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) → ¬ 𝑧 ∈ 𝑌 )
62 61 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ¬ 𝑧 ∈ 𝑌 )
63 eleq1w ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑌 ↔ 𝑧 ∈ 𝑌 ) )
64 63 notbid ⊢ ( 𝑤 = 𝑧 → ( ¬ 𝑤 ∈ 𝑌 ↔ ¬ 𝑧 ∈ 𝑌 ) )
65 62 64 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑤 = 𝑧 → ¬ 𝑤 ∈ 𝑌 ) )
66 65 con2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑤 ∈ 𝑌 → ¬ 𝑤 = 𝑧 ) )
67 66 imp ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ¬ 𝑤 = 𝑧 )
68 62 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ¬ 𝑧 ∈ 𝑌 )
69 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) )
70 69 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) )
71 70 breqd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑧 𝑅 𝑤 ↔ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) 𝑤 ) )
72 eldifi ⊢ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑧 ∈ 𝑋 )
73 72 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑧 ∈ 𝑋 )
74 73 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑧 ∈ 𝑋 )
75 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ 𝑌 )
76 brxp ⊢ ( 𝑧 ( 𝑋 × 𝑌 ) 𝑤 ↔ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) )
77 74 75 76 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑧 ( 𝑋 × 𝑌 ) 𝑤 )
78 brin ⊢ ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) 𝑤 ↔ ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ∧ 𝑧 ( 𝑋 × 𝑌 ) 𝑤 ) )
79 78 rbaib ⊢ ( 𝑧 ( 𝑋 × 𝑌 ) 𝑤 → ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) 𝑤 ↔ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) )
80 77 79 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) 𝑤 ↔ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) )
81 71 80 bitrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑧 𝑅 𝑤 ↔ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) )
82 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑌 𝑊 𝑅 ↔ ( ( 𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑅 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
83 82 biimpa ⊢ ( ( 𝜑 ∧ 𝑌 𝑊 𝑅 ) → ( ( 𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑅 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
84 83 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( ( 𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑅 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
85 84 simpld ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( 𝑌 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑌 × 𝑌 ) ) )
86 85 simprd ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑅 ⊆ ( 𝑌 × 𝑌 ) )
87 86 ad5ant12 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑅 ⊆ ( 𝑌 × 𝑌 ) )
88 87 ssbrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑧 𝑅 𝑤 → 𝑧 ( 𝑌 × 𝑌 ) 𝑤 ) )
89 brxp ⊢ ( 𝑧 ( 𝑌 × 𝑌 ) 𝑤 ↔ ( 𝑧 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) )
90 89 simplbi ⊢ ( 𝑧 ( 𝑌 × 𝑌 ) 𝑤 → 𝑧 ∈ 𝑌 )
91 88 90 syl6 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑧 𝑅 𝑤 → 𝑧 ∈ 𝑌 ) )
92 81 91 sylbird ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 → 𝑧 ∈ 𝑌 ) )
93 68 92 mtod ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 )
94 31 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑊 ‘ 𝑋 ) We 𝑋 )
95 weso ⊢ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 → ( 𝑊 ‘ 𝑋 ) Or 𝑋 )
96 94 95 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑊 ‘ 𝑋 ) Or 𝑋 )
97 13 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
98 97 sselda ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ 𝑋 )
99 sotric ⊢ ( ( ( 𝑊 ‘ 𝑋 ) Or 𝑋 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ↔ ¬ ( 𝑤 = 𝑧 ∨ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) ) )
100 ioran ⊢ ( ¬ ( 𝑤 = 𝑧 ∨ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) ↔ ( ¬ 𝑤 = 𝑧 ∧ ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) )
101 99 100 bitrdi ⊢ ( ( ( 𝑊 ‘ 𝑋 ) Or 𝑋 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ↔ ( ¬ 𝑤 = 𝑧 ∧ ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) ) )
102 96 98 74 101 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 ↔ ( ¬ 𝑤 = 𝑧 ∧ ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑤 ) ) )
103 67 93 102 mpbir2and ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 )
104 103 44 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) )
105 104 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑤 ∈ 𝑌 → 𝑤 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) )
106 105 ssrdv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑌 ⊆ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) )
107 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 )
108 106 107 eqssd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑌 = ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) )
109 in32 ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ∩ ( 𝑌 × 𝑌 ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) ∩ ( 𝑋 × 𝑌 ) )
110 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) )
111 110 ineq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑅 ∩ ( 𝑌 × 𝑌 ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ∩ ( 𝑌 × 𝑌 ) ) )
112 86 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑅 ⊆ ( 𝑌 × 𝑌 ) )
113 df-ss ⊢ ( 𝑅 ⊆ ( 𝑌 × 𝑌 ) ↔ ( 𝑅 ∩ ( 𝑌 × 𝑌 ) ) = 𝑅 )
114 112 113 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑅 ∩ ( 𝑌 × 𝑌 ) ) = 𝑅 )
115 111 114 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ∩ ( 𝑌 × 𝑌 ) ) = 𝑅 )
116 inss2 ⊢ ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) ⊆ ( 𝑌 × 𝑌 )
117 xpss1 ⊢ ( 𝑌 ⊆ 𝑋 → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑌 ) )
118 97 117 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑌 ) )
119 116 118 sstrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) ⊆ ( 𝑋 × 𝑌 ) )
120 df-ss ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) ⊆ ( 𝑋 × 𝑌 ) ↔ ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) ∩ ( 𝑋 × 𝑌 ) ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) )
121 119 120 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) ∩ ( 𝑋 × 𝑌 ) ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) )
122 109 115 121 3eqtr3a ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) )
123 108 sqxpeqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑌 × 𝑌 ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) )
124 123 ineq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑌 × 𝑌 ) ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ) )
125 122 124 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ) )
126 108 125 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑌 𝐹 𝑅 ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ) ) )
127 18 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝐴 ∈ 𝑉 )
128 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) )
129 128 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) )
130 1 127 129 fpwwe2lem3 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ) ) = 𝑧 )
131 73 130 mpdan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ) ) ) = 𝑧 )
132 126 131 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ( 𝑌 𝐹 𝑅 ) = 𝑧 )
133 132 62 eqneltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) ∧ ( 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∧ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 ) ) → ¬ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 )
134 133 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑧 } ) ⊆ 𝑌 → ¬ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) )
135 60 134 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ∃ 𝑧 ∈ ( 𝑋 ∖ 𝑌 ) ∀ 𝑤 ∈ ( 𝑋 ∖ 𝑌 ) ¬ 𝑤 ( 𝑊 ‘ 𝑋 ) 𝑧 → ¬ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) )
136 37 135 syld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑋 ∖ 𝑌 ) ≠ ∅ → ¬ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) )
137 136 necon4ad ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 → ( 𝑋 ∖ 𝑌 ) = ∅ ) )
138 16 137 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → ( 𝑋 ∖ 𝑌 ) = ∅ )
139 ssdif0 ⊢ ( 𝑋 ⊆ 𝑌 ↔ ( 𝑋 ∖ 𝑌 ) = ∅ )
140 138 139 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) → 𝑋 ⊆ 𝑌 )
141 140 ex ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) → 𝑋 ⊆ 𝑌 ) )
142 3 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
143 simprl ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑌 𝑊 𝑅 )
144 1 17 142 128 143 fpwwe2lem9 ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑊 ‘ 𝑋 ) = ( 𝑅 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌 ⊆ 𝑋 ∧ 𝑅 = ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑌 ) ) ) ) )
145 15 141 144 mpjaod ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑋 ⊆ 𝑌 )
146 13 145 eqssd ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑌 = 𝑋 )
147 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → Fun 𝑊 )
148 146 143 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑋 𝑊 𝑅 )
149 funbrfv ⊢ ( Fun 𝑊 → ( 𝑋 𝑊 𝑅 → ( 𝑊 ‘ 𝑋 ) = 𝑅 ) )
150 147 148 149 sylc ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( 𝑊 ‘ 𝑋 ) = 𝑅 )
151 150 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → 𝑅 = ( 𝑊 ‘ 𝑋 ) )
152 146 151 jca ⊢ ( ( 𝜑 ∧ ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) → ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) )
153 152 ex ⊢ ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) → ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) ) )
154 1 2 3 4 fpwwe2lem12 ⊢ ( 𝜑 → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
155 22 154 jca ⊢ ( 𝜑 → ( 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ∧ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
156 breq12 ⊢ ( ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) → ( 𝑌 𝑊 𝑅 ↔ 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ) )
157 oveq12 ⊢ ( ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) → ( 𝑌 𝐹 𝑅 ) = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
158 simpl ⊢ ( ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) → 𝑌 = 𝑋 )
159 157 158 eleq12d ⊢ ( ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) → ( ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ↔ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
160 156 159 anbi12d ⊢ ( ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ↔ ( 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ∧ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ) )
161 155 160 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) → ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ) )
162 153 161 impbid ⊢ ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 𝐹 𝑅 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) ) )