fpwwe2

Description: Given any function F from well-orderings of subsets of A to A , there is a unique well-ordered subset <. X , ( WX ) >. which "agrees" with F in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a . Theorem 1.1 of KanamoriPincus p. 415. (Contributed by Mario Carneiro, 18-May-2015) (Revised by AV, 20-Jul-2024)

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

Proof

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

Metamath Proof Explorer

Theorem fpwwe2

Proof