Metamath Proof Explorer

Theorem fpwwe2lem12

Description: Lemma for fpwwe2 . (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 fpwwe2lem12 ( 𝜑 → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2.4 ⊢ 𝑋 = ∪ dom 𝑊
5 ssun2 ⊢ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
6 2 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → 𝐴 ∈ 𝑉 )
7 3 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
8 1 6 7 4 fpwwe2lem11 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → 𝑋 ∈ dom 𝑊 )
9 1 6 7 4 fpwwe2lem10 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → 𝑊 : dom 𝑊 ⟶ 𝒫 ( 𝑋 × 𝑋 ) )
10 ffun ⊢ ( 𝑊 : dom 𝑊 ⟶ 𝒫 ( 𝑋 × 𝑋 ) → Fun 𝑊 )
11 funfvbrb ⊢ ( Fun 𝑊 → ( 𝑋 ∈ dom 𝑊 ↔ 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ) )
12 9 10 11 3syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ∈ dom 𝑊 ↔ 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ) )
13 8 12 mpbid ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) )
14 1 6 fpwwe2lem2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 𝑊 ( 𝑊 ‘ 𝑋 ) ↔ ( ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
15 13 14 mpbid ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
16 15 simpld ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → 𝑋 ⊆ 𝐴 )
18 16 simprd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) )
19 15 simprd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑊 ‘ 𝑋 ) We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
20 19 simpld ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑊 ‘ 𝑋 ) We 𝑋 )
21 17 18 20 3jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ∧ ( 𝑊 ‘ 𝑋 ) We 𝑋 ) )
22 1 2 3 fpwwe2lem4 ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ∧ ( 𝑊 ‘ 𝑋 ) We 𝑋 ) ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝐴 )
23 21 22 syldan ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝐴 )
24 23 snssd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ 𝐴 )
25 17 24 unssd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝐴 )
26 ssun1 ⊢ 𝑋 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
27 xpss12 ⊢ ( ( 𝑋 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑋 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑋 × 𝑋 ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
28 26 26 27 mp2an ⊢ ( 𝑋 × 𝑋 ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
29 18 28 sstrdi ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
30 xpss12 ⊢ ( ( 𝑋 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
31 26 5 30 mp2an ⊢ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
32 31 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
33 29 32 unssd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
34 25 33 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝐴 ∧ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ) )
35 ssdif0 ⊢ ( 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ↔ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ∅ )
36 simpllr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
37 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) )
38 37 ssbrd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) )
39 brxp ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ∧ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
40 39 simplbi ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
41 38 40 syl6 ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
42 36 41 mtod ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
43 brxp ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ∧ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
44 43 simplbi ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
45 36 44 nsyl ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
46 ovex ⊢ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ V
47 breq2 ⊢ ( 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) )
48 brun ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) )
49 47 48 bitrdi ⊢ ( 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) ) )
50 49 notbid ⊢ ( 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) ) )
51 46 50 rexsn ⊢ ( ∃ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) )
52 ioran ⊢ ( ¬ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) ↔ ( ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) )
53 51 52 bitri ⊢ ( ∃ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) )
54 42 45 53 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ∃ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
55 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
56 sssn ⊢ ( 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
57 55 56 sylib ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑥 = ∅ ∨ 𝑥 = { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
58 simplrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → 𝑥 ≠ ∅ )
59 58 neneqd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ 𝑥 = ∅ )
60 57 59 orcnd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → 𝑥 = { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
61 60 raleqdv ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
62 breq1 ⊢ ( 𝑧 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
63 62 notbid ⊢ ( 𝑧 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
64 46 63 ralsn ⊢ ( ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
65 61 64 bitrdi ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
66 60 65 rexeqbidv ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ∃ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
67 54 66 mpbird ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
68 67 ex ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) → ( 𝑥 ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
69 35 68 syl5bir ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) → ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ∅ → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
70 vex ⊢ 𝑥 ∈ V
71 difexg ⊢ ( 𝑥 ∈ V → ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ V )
72 70 71 mp1i ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ V )
73 wefr ⊢ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 → ( 𝑊 ‘ 𝑋 ) Fr 𝑋 )
74 20 73 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑊 ‘ 𝑋 ) Fr 𝑋 )
75 74 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ( 𝑊 ‘ 𝑋 ) Fr 𝑋 )
76 simplrl ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
77 uncom ⊢ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∪ 𝑋 )
78 76 77 sseqtrdi ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → 𝑥 ⊆ ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∪ 𝑋 ) )
79 ssundif ⊢ ( 𝑥 ⊆ ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∪ 𝑋 ) ↔ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝑋 )
80 78 79 sylib ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝑋 )
81 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ )
82 fri ⊢ ( ( ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ V ∧ ( 𝑊 ‘ 𝑋 ) Fr 𝑋 ) ∧ ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝑋 ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ) → ∃ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 )
83 72 75 80 81 82 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 )
84 brun ⊢ ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) )
85 idd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
86 brxp ⊢ ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ↔ ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
87 86 simprbi ⊢ ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 → 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
88 eldifn ⊢ ( 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
89 88 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ¬ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
90 89 pm2.21d ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } → 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
91 87 90 syl5 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 → 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
92 85 91 jaod ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) → 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
93 84 92 syl5bi ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 → 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
94 93 con3d ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
95 94 ralimdv ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
96 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
97 96 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
98 18 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) )
99 98 ssbrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × 𝑋 ) 𝑦 ) )
100 brxp ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × 𝑋 ) 𝑦 ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
101 100 simplbi ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × 𝑋 ) 𝑦 → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
102 99 101 syl6 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
103 97 102 mtod ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 )
104 brxp ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
105 104 simprbi ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 → 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
106 89 105 nsyl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 )
107 brun ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) )
108 62 107 bitrdi ⊢ ( 𝑧 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) ) )
109 108 notbid ⊢ ( 𝑧 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ( ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) ) )
110 46 109 ralsn ⊢ ( ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ¬ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) )
111 ioran ⊢ ( ¬ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) ↔ ( ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) )
112 110 111 bitri ⊢ ( ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ ( ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑊 ‘ 𝑋 ) 𝑦 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) )
113 103 106 112 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
114 95 113 jctird ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∧ ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) ) )
115 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
116 undif1 ⊢ ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( 𝑥 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
117 115 116 sseqtrri ⊢ 𝑥 ⊆ ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
118 ralun ⊢ ( ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∧ ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) → ∀ 𝑧 ∈ ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
119 ssralv ⊢ ( 𝑥 ⊆ ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ∀ 𝑧 ∈ ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
120 117 118 119 mpsyl ⊢ ( ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∧ ∀ 𝑧 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
121 114 120 syl6 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
122 eldifi ⊢ ( 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → 𝑦 ∈ 𝑥 )
123 122 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → 𝑦 ∈ 𝑥 )
124 121 123 jctild ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) ) )
125 124 expimpd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ( ( 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) → ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) ) )
126 125 reximdv2 ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ( ∃ 𝑦 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∀ 𝑧 ∈ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ¬ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
127 83 126 mpd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) ∧ ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
128 127 ex ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) → ( ( 𝑥 ∖ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ≠ ∅ → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
129 69 128 pm2.61dne ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
130 129 ex ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
131 130 alrimiv ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ∀ 𝑥 ( ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
132 df-fr ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) Fr ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↔ ∀ 𝑥 ( ( 𝑥 ⊆ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
133 131 132 sylibr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) Fr ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
134 elun ⊢ ( 𝑥 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
135 elun ⊢ ( 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↔ ( 𝑦 ∈ 𝑋 ∨ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
136 134 135 anbi12i ⊢ ( ( 𝑥 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∨ 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ( 𝑦 ∈ 𝑋 ∨ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
137 weso ⊢ ( ( 𝑊 ‘ 𝑋 ) We 𝑋 → ( 𝑊 ‘ 𝑋 ) Or 𝑋 )
138 20 137 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑊 ‘ 𝑋 ) Or 𝑋 )
139 solin ⊢ ( ( ( 𝑊 ‘ 𝑋 ) Or 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( 𝑊 ‘ 𝑋 ) 𝑥 ) )
140 138 139 sylan ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( 𝑊 ‘ 𝑋 ) 𝑥 ) )
141 ssun1 ⊢ ( 𝑊 ‘ 𝑋 ) ⊆ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
142 141 a1i ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
143 142 ssbrd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( 𝑊 ‘ 𝑋 ) 𝑦 → 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
144 idd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
145 142 ssbrd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 ( 𝑊 ‘ 𝑋 ) 𝑥 → 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
146 143 144 145 3orim123d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( 𝑊 ‘ 𝑋 ) 𝑥 ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
147 140 146 mpd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
148 147 ex ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
149 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ 𝑋 ) )
150 149 ancomd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
151 brxp ⊢ ( 𝑦 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑥 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
152 150 151 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑥 )
153 ssun2 ⊢ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
154 153 ssbri ⊢ ( 𝑦 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑥 → 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 )
155 3mix3 ⊢ ( 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
156 152 154 155 3syl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
157 156 ex ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
158 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
159 brxp ⊢ ( 𝑥 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
160 158 159 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → 𝑥 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 )
161 153 ssbri ⊢ ( 𝑥 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 → 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
162 3mix1 ⊢ ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
163 160 161 162 3syl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
164 163 ex ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
165 elsni ⊢ ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } → 𝑥 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
166 elsni ⊢ ( 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } → 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
167 eqtr3 ⊢ ( ( 𝑥 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∧ 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ) → 𝑥 = 𝑦 )
168 165 166 167 syl2an ⊢ ( ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → 𝑥 = 𝑦 )
169 168 3mix2d ⊢ ( ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
170 169 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
171 148 157 164 170 ccased ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( ( 𝑥 ∈ 𝑋 ∨ 𝑥 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ( 𝑦 ∈ 𝑋 ∨ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
172 136 171 syl5bi ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑥 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
173 172 ralrimivv ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ∀ 𝑥 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∀ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) )
174 dfwe2 ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) We ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↔ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) Fr ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∀ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ( 𝑥 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑥 ) ) )
175 133 173 174 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) We ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
176 1 fpwwe2cbv ⊢ 𝑊 = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑏 ] ( 𝑏 𝐹 ( 𝑠 ∩ ( 𝑏 × 𝑏 ) ) ) = 𝑧 ) ) }
177 176 6 13 fpwwe2lem3 ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ) = 𝑦 )
178 cnvimass ⊢ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ⊆ dom ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
179 fvex ⊢ ( 𝑊 ‘ 𝑋 ) ∈ V
180 snex ⊢ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∈ V
181 xpexg ⊢ ( ( 𝑋 ∈ dom 𝑊 ∧ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∈ V ) → ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ V )
182 8 180 181 sylancl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ V )
183 unexg ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∈ V ∧ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ V ) → ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∈ V )
184 179 182 183 sylancr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∈ V )
185 184 dmexd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → dom ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∈ V )
186 ssexg ⊢ ( ( ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ⊆ dom ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∧ dom ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∈ V ) → ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ∈ V )
187 178 185 186 sylancr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ∈ V )
188 187 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ∈ V )
189 id ⊢ ( 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) → 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) )
190 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
191 simplr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
192 nelne2 ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → 𝑦 ≠ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
193 190 191 192 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ≠ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
194 87 166 syl ⊢ ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 → 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
195 194 necon3ai ⊢ ( 𝑦 ≠ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) → ¬ 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 )
196 biorf ⊢ ( ¬ 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 → ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ↔ ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ∨ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) ) )
197 193 195 196 3syl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ↔ ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ∨ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) ) )
198 orcom ⊢ ( ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ∨ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) ↔ ( 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ∨ 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ) )
199 198 84 bitr4i ⊢ ( ( 𝑧 ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑦 ∨ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) ↔ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
200 197 199 bitr2di ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ↔ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
201 vex ⊢ 𝑧 ∈ V
202 201 eliniseg ⊢ ( 𝑦 ∈ V → ( 𝑧 ∈ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ↔ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 ) )
203 202 elv ⊢ ( 𝑧 ∈ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ↔ 𝑧 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) 𝑦 )
204 201 eliniseg ⊢ ( 𝑦 ∈ V → ( 𝑧 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ↔ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 ) )
205 204 elv ⊢ ( 𝑧 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ↔ 𝑧 ( 𝑊 ‘ 𝑋 ) 𝑦 )
206 200 203 205 3bitr4g ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ∈ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ↔ 𝑧 ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) )
207 206 eqrdv ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) = ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) )
208 189 207 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → 𝑢 = ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) )
209 208 sqxpeqd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( 𝑢 × 𝑢 ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) )
210 209 ineq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) )
211 indir ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ∪ ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) )
212 inxp ⊢ ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) × ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) )
213 incom ⊢ ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ∩ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
214 cnvimass ⊢ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ⊆ dom ( 𝑊 ‘ 𝑋 )
215 18 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) )
216 dmss ⊢ ( ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) → dom ( 𝑊 ‘ 𝑋 ) ⊆ dom ( 𝑋 × 𝑋 ) )
217 215 216 syl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → dom ( 𝑊 ‘ 𝑋 ) ⊆ dom ( 𝑋 × 𝑋 ) )
218 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
219 217 218 sseqtrdi ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → dom ( 𝑊 ‘ 𝑋 ) ⊆ 𝑋 )
220 214 219 sstrid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ⊆ 𝑋 )
221 220 191 ssneldd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) )
222 disjsn ⊢ ( ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ∩ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ∅ ↔ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) )
223 221 222 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ∩ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ∅ )
224 213 223 eqtrid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) = ∅ )
225 224 xpeq2d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) × ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) × ∅ ) )
226 xp0 ⊢ ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) × ∅ ) = ∅
227 225 226 eqtrdi ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑋 ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) × ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ∅ )
228 212 227 eqtrid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ∅ )
229 228 uneq2d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ∪ ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ∪ ∅ ) )
230 211 229 eqtrid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ∪ ∅ ) )
231 un0 ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ∪ ∅ ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) )
232 230 231 eqtrdi ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) )
233 232 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) )
234 210 233 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) = ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) )
235 208 234 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ) )
236 235 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ) = 𝑦 ) )
237 188 236 sbcied ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) 𝐹 ( ( 𝑊 ‘ 𝑋 ) ∩ ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) × ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ) ) ) = 𝑦 ) )
238 177 237 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
239 166 adantl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → 𝑦 = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
240 239 eqcomd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) = 𝑦 )
241 187 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ∈ V )
242 simplr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
243 239 eleq1d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑦 ∈ dom ◡ ( 𝑊 ‘ 𝑋 ) ↔ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ dom ◡ ( 𝑊 ‘ 𝑋 ) ) )
244 18 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) )
245 rnss ⊢ ( ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) → ran ( 𝑊 ‘ 𝑋 ) ⊆ ran ( 𝑋 × 𝑋 ) )
246 244 245 syl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ran ( 𝑊 ‘ 𝑋 ) ⊆ ran ( 𝑋 × 𝑋 ) )
247 df-rn ⊢ ran ( 𝑊 ‘ 𝑋 ) = dom ◡ ( 𝑊 ‘ 𝑋 )
248 rnxpid ⊢ ran ( 𝑋 × 𝑋 ) = 𝑋
249 246 247 248 3sstr3g ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → dom ◡ ( 𝑊 ‘ 𝑋 ) ⊆ 𝑋 )
250 249 sseld ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ dom ◡ ( 𝑊 ‘ 𝑋 ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
251 243 250 sylbid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑦 ∈ dom ◡ ( 𝑊 ‘ 𝑋 ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) )
252 242 251 mtod ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ¬ 𝑦 ∈ dom ◡ ( 𝑊 ‘ 𝑋 ) )
253 ndmima ⊢ ( ¬ 𝑦 ∈ dom ◡ ( 𝑊 ‘ 𝑋 ) → ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) = ∅ )
254 252 253 syl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) = ∅ )
255 239 sneqd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → { 𝑦 } = { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
256 255 imaeq2d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { 𝑦 } ) = ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
257 df-ima ⊢ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ran ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
258 cnvxp ⊢ ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 )
259 258 reseq1i ⊢ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
260 ssid ⊢ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) }
261 xpssres ⊢ ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } → ( ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 ) )
262 260 261 ax-mp ⊢ ( ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 )
263 259 262 eqtri ⊢ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 )
264 263 rneqi ⊢ ran ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ran ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 )
265 46 snnz ⊢ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ≠ ∅
266 rnxp ⊢ ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ≠ ∅ → ran ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 ) = 𝑋 )
267 265 266 ax-mp ⊢ ran ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } × 𝑋 ) = 𝑋
268 264 267 eqtri ⊢ ran ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ↾ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = 𝑋
269 257 268 eqtri ⊢ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = 𝑋
270 256 269 eqtrdi ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { 𝑦 } ) = 𝑋 )
271 254 270 uneq12d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ∪ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { 𝑦 } ) ) = ( ∅ ∪ 𝑋 ) )
272 cnvun ⊢ ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) = ( ◡ ( 𝑊 ‘ 𝑋 ) ∪ ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) )
273 272 imaeq1i ⊢ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) ∪ ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } )
274 imaundir ⊢ ( ( ◡ ( 𝑊 ‘ 𝑋 ) ∪ ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ∪ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { 𝑦 } ) )
275 273 274 eqtri ⊢ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) = ( ( ◡ ( 𝑊 ‘ 𝑋 ) “ { 𝑦 } ) ∪ ( ◡ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) “ { 𝑦 } ) )
276 un0 ⊢ ( 𝑋 ∪ ∅ ) = 𝑋
277 uncom ⊢ ( 𝑋 ∪ ∅ ) = ( ∅ ∪ 𝑋 )
278 276 277 eqtr3i ⊢ 𝑋 = ( ∅ ∪ 𝑋 )
279 271 275 278 3eqtr4g ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) = 𝑋 )
280 189 279 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → 𝑢 = 𝑋 )
281 280 sqxpeqd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( 𝑢 × 𝑢 ) = ( 𝑋 × 𝑋 ) )
282 281 ineq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑋 × 𝑋 ) ) )
283 indir ⊢ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑋 × 𝑋 ) ) = ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑋 ) ) ∪ ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( 𝑋 × 𝑋 ) ) )
284 df-ss ⊢ ( ( 𝑊 ‘ 𝑋 ) ⊆ ( 𝑋 × 𝑋 ) ↔ ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑋 ) ) = ( 𝑊 ‘ 𝑋 ) )
285 244 284 sylib ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑋 ) ) = ( 𝑊 ‘ 𝑋 ) )
286 incom ⊢ ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ 𝑋 ) = ( 𝑋 ∩ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } )
287 disjsn ⊢ ( ( 𝑋 ∩ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ∅ ↔ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
288 242 287 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑋 ∩ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) = ∅ )
289 286 288 eqtrid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ 𝑋 ) = ∅ )
290 289 xpeq2d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( 𝑋 × ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ 𝑋 ) ) = ( 𝑋 × ∅ ) )
291 xpindi ⊢ ( 𝑋 × ( { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ∩ 𝑋 ) ) = ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( 𝑋 × 𝑋 ) )
292 xp0 ⊢ ( 𝑋 × ∅ ) = ∅
293 290 291 292 3eqtr3g ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( 𝑋 × 𝑋 ) ) = ∅ )
294 285 293 uneq12d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( ( 𝑊 ‘ 𝑋 ) ∩ ( 𝑋 × 𝑋 ) ) ∪ ( ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∩ ( 𝑋 × 𝑋 ) ) ) = ( ( 𝑊 ‘ 𝑋 ) ∪ ∅ ) )
295 283 294 eqtrid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑋 × 𝑋 ) ) = ( ( 𝑊 ‘ 𝑋 ) ∪ ∅ ) )
296 un0 ⊢ ( ( 𝑊 ‘ 𝑋 ) ∪ ∅ ) = ( 𝑊 ‘ 𝑋 )
297 295 296 eqtrdi ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑋 × 𝑋 ) ) = ( 𝑊 ‘ 𝑋 ) )
298 297 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑋 × 𝑋 ) ) = ( 𝑊 ‘ 𝑋 ) )
299 282 298 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) = ( 𝑊 ‘ 𝑋 ) )
300 280 299 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) )
301 300 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ 𝑢 = ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) ) → ( ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) = 𝑦 ) )
302 241 301 sbcied ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → ( [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) = 𝑦 ) )
303 240 302 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) → [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
304 238 303 jaodan ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∨ 𝑦 ∈ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
305 135 304 sylan2b ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
306 305 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ∀ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
307 175 306 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) We ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
308 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑊 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ↔ ( ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝐴 ∧ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ) ∧ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) We ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
309 308 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑊 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ↔ ( ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝐴 ∧ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ⊆ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) × ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ) ∧ ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) We ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) [ ( ◡ ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
310 34 307 309 mpbir2and ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑊 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) )
311 1 relopabiv ⊢ Rel 𝑊
312 311 releldmi ⊢ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) 𝑊 ( ( 𝑊 ‘ 𝑋 ) ∪ ( 𝑋 × { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ) → ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ dom 𝑊 )
313 elssuni ⊢ ( ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ∈ dom 𝑊 → ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ ∪ dom 𝑊 )
314 310 312 313 3syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ ∪ dom 𝑊 )
315 314 4 sseqtrrdi ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 ∪ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ) ⊆ 𝑋 )
316 5 315 sstrid ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ 𝑋 )
317 46 snss ⊢ ( ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ↔ { ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) } ⊆ 𝑋 )
318 316 317 sylibr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 ) → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )
319 318 pm2.18da ⊢ ( 𝜑 → ( 𝑋 𝐹 ( 𝑊 ‘ 𝑋 ) ) ∈ 𝑋 )