Metamath Proof Explorer

Theorem fvineqsneq

Description: A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 28-Mar-2021)

Ref Expression
Assertion fvineqsneq ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑍 ⊆ ran 𝐹 ∧ 𝐴 ⊆ ∪ 𝑍 ) ) → 𝑍 = ran 𝐹 )

Proof

Step Hyp Ref Expression
1 pssnel ⊢ ( 𝑍 ⊊ ran 𝐹 → ∃ 𝑥 ( 𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ 𝑍 ) )
2 1 adantl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑥 ( 𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ 𝑍 ) )
3 df-rex ⊢ ( ∃ 𝑥 ∈ ran 𝐹 ¬ 𝑥 ∈ 𝑍 ↔ ∃ 𝑥 ( 𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ 𝑍 ) )
4 2 3 sylibr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑥 ∈ ran 𝐹 ¬ 𝑥 ∈ 𝑍 )
5 fnrnfv ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑥 ∣ ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) } )
6 5 eqabrd ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) )
7 6 biimpd ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ran 𝐹 → ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) )
8 7 ralrimiv ⊢ ( 𝐹 Fn 𝐴 → ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) )
9 8 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) )
10 9 adantr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) )
11 r19.29r ⊢ ( ( ∃ 𝑥 ∈ ran 𝐹 ¬ 𝑥 ∈ 𝑍 ∧ ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) → ∃ 𝑥 ∈ ran 𝐹 ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) )
12 4 10 11 syl2anc ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑥 ∈ ran 𝐹 ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) )
13 nfra1 ⊢ Ⅎ 𝑝 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 }
14 rsp ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) )
15 vsnid ⊢ 𝑝 ∈ { 𝑝 }
16 eleq2 ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) ↔ 𝑝 ∈ { 𝑝 } ) )
17 15 16 mpbiri ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → 𝑝 ∈ ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) )
18 17 elin1d ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → 𝑝 ∈ ( 𝐹 ‘ 𝑝 ) )
19 14 18 syl6 ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( 𝐹 ‘ 𝑝 ) ) )
20 19 adantr ⊢ ( ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ 𝑥 = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( 𝐹 ‘ 𝑝 ) ) )
21 eleq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑝 ) → ( 𝑝 ∈ 𝑥 ↔ 𝑝 ∈ ( 𝐹 ‘ 𝑝 ) ) )
22 21 adantl ⊢ ( ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ 𝑥 = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑝 ∈ 𝑥 ↔ 𝑝 ∈ ( 𝐹 ‘ 𝑝 ) ) )
23 20 22 sylibrd ⊢ ( ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ 𝑥 = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝑥 ) )
24 23 ex ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑥 = ( 𝐹 ‘ 𝑝 ) → ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝑥 ) ) )
25 24 com23 ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( 𝑝 ∈ 𝐴 → ( 𝑥 = ( 𝐹 ‘ 𝑝 ) → 𝑝 ∈ 𝑥 ) ) )
26 13 25 reximdai ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) )
27 26 adantl ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) )
28 27 adantr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) )
29 28 anim2d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) → ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) ) )
30 29 reximdv ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ∃ 𝑥 ∈ ran 𝐹 ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑥 = ( 𝐹 ‘ 𝑝 ) ) → ∃ 𝑥 ∈ ran 𝐹 ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) ) )
31 12 30 mpd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑥 ∈ ran 𝐹 ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) )
32 ancom ⊢ ( ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) ↔ ( ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
33 r19.41v ⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ↔ ( ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
34 32 33 bitr4i ⊢ ( ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
35 34 rexbii ⊢ ( ∃ 𝑥 ∈ ran 𝐹 ( ¬ 𝑥 ∈ 𝑍 ∧ ∃ 𝑝 ∈ 𝐴 𝑝 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
36 31 35 sylib ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
37 rexcom ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ↔ ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑝 ∈ 𝐴 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
38 36 37 sylibr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
39 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 )
40 39 19.3 ⊢ ( ∀ 𝑥 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ↔ ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
41 alral ⊢ ( ∀ 𝑥 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
42 40 41 sylbir ⊢ ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
43 42 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
44 38 43 syl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) )
45 nfv ⊢ Ⅎ 𝑝 𝐹 Fn 𝐴
46 45 13 nfan ⊢ Ⅎ 𝑝 ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
47 nfv ⊢ Ⅎ 𝑝 𝑍 ⊊ ran 𝐹
48 46 47 nfan ⊢ Ⅎ 𝑝 ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 )
49 nfv ⊢ Ⅎ 𝑥 ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ 𝑝 ∈ 𝐴 )
50 fvineqsneu ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 )
51 50 adantr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∀ 𝑝 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 )
52 rsp ⊢ ( ∀ 𝑝 ∈ 𝐴 ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 → ( 𝑝 ∈ 𝐴 → ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ) )
53 51 52 syl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( 𝑝 ∈ 𝐴 → ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ) )
54 53 adantrd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑥 ∈ ran 𝐹 ) → ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ) )
55 54 imp ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑥 ∈ ran 𝐹 ) ) → ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 )
56 reupick3 ⊢ ( ( ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ∧ ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ∧ 𝑥 ∈ ran 𝐹 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) )
57 56 3expa ⊢ ( ( ( ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ∧ ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ) ∧ 𝑥 ∈ ran 𝐹 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) )
58 57 expcom ⊢ ( 𝑥 ∈ ran 𝐹 → ( ( ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ∧ ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
59 58 adantl ⊢ ( ( 𝑝 ∈ 𝐴 ∧ 𝑥 ∈ ran 𝐹 ) → ( ( ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ∧ ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
60 59 adantl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑥 ∈ ran 𝐹 ) ) → ( ( ∃! 𝑥 ∈ ran 𝐹 𝑝 ∈ 𝑥 ∧ ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
61 55 60 mpand ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑥 ∈ ran 𝐹 ) ) → ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
62 61 expr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑥 ∈ ran 𝐹 → ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) )
63 49 62 ralrimi ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ 𝑝 ∈ 𝐴 ) → ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
64 63 ex ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( 𝑝 ∈ 𝐴 → ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) )
65 48 64 ralrimi ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∀ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
66 r19.29r ⊢ ( ( ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) )
67 44 65 66 syl2anc ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) )
68 ralim ⊢ ( ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) → ( ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) )
69 68 impcom ⊢ ( ( ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) → ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) )
70 69 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑥 ∈ ran 𝐹 ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ( ∃ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 ∧ ¬ 𝑥 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) )
71 67 70 syl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) )
72 con2b ⊢ ( ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ↔ ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) )
73 72 ralbii ⊢ ( ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ↔ ∀ 𝑥 ∈ ran 𝐹 ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) )
74 df-ral ⊢ ( ∀ 𝑥 ∈ ran 𝐹 ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ran 𝐹 → ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) ) )
75 bi2.04 ⊢ ( ( 𝑥 ∈ ran 𝐹 → ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
76 75 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ran 𝐹 → ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
77 73 74 76 3bitri ⊢ ( ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
78 77 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) )
79 48 78 rexbid ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ ran 𝐹 ( 𝑝 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑍 ) ↔ ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) )
80 71 79 mpbid ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
81 nfv ⊢ Ⅎ 𝑥 ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 )
82 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) )
83 81 82 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
84 pssss ⊢ ( 𝑍 ⊊ ran 𝐹 → 𝑍 ⊆ ran 𝐹 )
85 df-ss ⊢ ( 𝑍 ⊆ ran 𝐹 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ran 𝐹 ) )
86 84 85 sylib ⊢ ( 𝑍 ⊊ ran 𝐹 → ∀ 𝑥 ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ran 𝐹 ) )
87 86 adantl ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∀ 𝑥 ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ran 𝐹 ) )
88 df-ral ⊢ ( ∀ 𝑥 ∈ 𝑍 𝑥 ∈ ran 𝐹 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ran 𝐹 ) )
89 87 88 sylibr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∀ 𝑥 ∈ 𝑍 𝑥 ∈ ran 𝐹 )
90 89 adantr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑍 𝑥 ∈ ran 𝐹 )
91 rsp ⊢ ( ∀ 𝑥 ∈ 𝑍 𝑥 ∈ ran 𝐹 → ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ran 𝐹 ) )
92 90 91 syl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) → ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ran 𝐹 ) )
93 df-ral ⊢ ( ∀ 𝑥 ∈ 𝑍 ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
94 93 biimpri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑍 ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) )
95 94 adantl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑍 ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) )
96 rsp ⊢ ( ∀ 𝑥 ∈ 𝑍 ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
97 95 96 syl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) → ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) )
98 92 97 mpdd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) → ( 𝑥 ∈ 𝑍 → ¬ 𝑝 ∈ 𝑥 ) )
99 83 98 ralrimi ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 )
100 99 ex ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 ) )
101 100 a1d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( 𝑝 ∈ 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 ) ) )
102 48 101 reximdai ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ( ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ( 𝑥 ∈ 𝑍 → ( 𝑥 ∈ ran 𝐹 → ¬ 𝑝 ∈ 𝑥 ) ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 ) )
103 80 102 mpd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 )
104 ralnex ⊢ ( ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 ↔ ¬ ∃ 𝑥 ∈ 𝑍 𝑝 ∈ 𝑥 )
105 104 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∀ 𝑥 ∈ 𝑍 ¬ 𝑝 ∈ 𝑥 ↔ ∃ 𝑝 ∈ 𝐴 ¬ ∃ 𝑥 ∈ 𝑍 𝑝 ∈ 𝑥 )
106 103 105 sylib ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ¬ ∃ 𝑥 ∈ 𝑍 𝑝 ∈ 𝑥 )
107 eluni2 ⊢ ( 𝑝 ∈ ∪ 𝑍 ↔ ∃ 𝑥 ∈ 𝑍 𝑝 ∈ 𝑥 )
108 107 notbii ⊢ ( ¬ 𝑝 ∈ ∪ 𝑍 ↔ ¬ ∃ 𝑥 ∈ 𝑍 𝑝 ∈ 𝑥 )
109 108 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ∈ ∪ 𝑍 ↔ ∃ 𝑝 ∈ 𝐴 ¬ ∃ 𝑥 ∈ 𝑍 𝑝 ∈ 𝑥 )
110 106 109 sylibr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ∈ ∪ 𝑍 )
111 dfss3 ⊢ ( 𝐴 ⊆ ∪ 𝑍 ↔ ∀ 𝑝 ∈ 𝐴 𝑝 ∈ ∪ 𝑍 )
112 dfral2 ⊢ ( ∀ 𝑝 ∈ 𝐴 𝑝 ∈ ∪ 𝑍 ↔ ¬ ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ∈ ∪ 𝑍 )
113 111 112 bitri ⊢ ( 𝐴 ⊆ ∪ 𝑍 ↔ ¬ ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ∈ ∪ 𝑍 )
114 113 con2bii2 ⊢ ( ¬ 𝐴 ⊆ ∪ 𝑍 ↔ ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ∈ ∪ 𝑍 )
115 110 114 sylibr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ 𝑍 ⊊ ran 𝐹 ) → ¬ 𝐴 ⊆ ∪ 𝑍 )
116 115 ex ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑍 ⊊ ran 𝐹 → ¬ 𝐴 ⊆ ∪ 𝑍 ) )
117 116 con2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝐴 ⊆ ∪ 𝑍 → ¬ 𝑍 ⊊ ran 𝐹 ) )
118 npss ⊢ ( ¬ 𝑍 ⊊ ran 𝐹 ↔ ( 𝑍 ⊆ ran 𝐹 → 𝑍 = ran 𝐹 ) )
119 117 118 imbitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝐴 ⊆ ∪ 𝑍 → ( 𝑍 ⊆ ran 𝐹 → 𝑍 = ran 𝐹 ) ) )
120 119 com23 ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝑍 ⊆ ran 𝐹 → ( 𝐴 ⊆ ∪ 𝑍 → 𝑍 = ran 𝐹 ) ) )
121 120 imp32 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) ∧ ( 𝑍 ⊆ ran 𝐹 ∧ 𝐴 ⊆ ∪ 𝑍 ) ) → 𝑍 = ran 𝐹 )