This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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