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)

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

Proof

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