Metamath Proof Explorer

Theorem bnj1398

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1398.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1398.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1398.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1398.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
bnj1398.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
bnj1398.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
bnj1398.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
bnj1398.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
bnj1398.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
bnj1398.10 ⊢ 𝑃 = ∪ 𝐻
bnj1398.11 ⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
bnj1398.12 ⊢ ( 𝜂 ↔ ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
Assertion bnj1398 ( 𝜒 → ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = dom 𝑃 )

Proof

Step Hyp Ref Expression
1 bnj1398.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1398.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1398.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1398.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5 bnj1398.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6 bnj1398.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
7 bnj1398.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1398.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
9 bnj1398.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10 bnj1398.10 ⊢ 𝑃 = ∪ 𝐻
11 bnj1398.11 ⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12 bnj1398.12 ⊢ ( 𝜂 ↔ ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
13 df-iun ⊢ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) }
14 13 bnj1436 ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
15 11 14 simplbiim ⊢ ( 𝜃 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
16 nfv ⊢ Ⅎ 𝑦 𝜓
17 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐷
18 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥
19 16 17 18 nf3an ⊢ Ⅎ 𝑦 ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 )
20 7 19 nfxfr ⊢ Ⅎ 𝑦 𝜒
21 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
22 21 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
23 20 22 nfan ⊢ Ⅎ 𝑦 ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
24 11 23 nfxfr ⊢ Ⅎ 𝑦 𝜃
25 24 nf5ri ⊢ ( 𝜃 → ∀ 𝑦 𝜃 )
26 15 12 25 bnj1521 ⊢ ( 𝜃 → ∃ 𝑦 𝜂 )
27 nfv ⊢ Ⅎ 𝑓 𝑅 FrSe 𝐴
28 nfe1 ⊢ Ⅎ 𝑓 ∃ 𝑓 𝜏
29 28 nfn ⊢ Ⅎ 𝑓 ¬ ∃ 𝑓 𝜏
30 nfcv ⊢ Ⅎ 𝑓 𝐴
31 29 30 nfrabw ⊢ Ⅎ 𝑓 { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
32 5 31 nfcxfr ⊢ Ⅎ 𝑓 𝐷
33 nfcv ⊢ Ⅎ 𝑓 ∅
34 32 33 nfne ⊢ Ⅎ 𝑓 𝐷 ≠ ∅
35 27 34 nfan ⊢ Ⅎ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ )
36 6 35 nfxfr ⊢ Ⅎ 𝑓 𝜓
37 32 nfcri ⊢ Ⅎ 𝑓 𝑥 ∈ 𝐷
38 nfv ⊢ Ⅎ 𝑓 ¬ 𝑦 𝑅 𝑥
39 32 38 nfralw ⊢ Ⅎ 𝑓 ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥
40 36 37 39 nf3an ⊢ Ⅎ 𝑓 ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 )
41 7 40 nfxfr ⊢ Ⅎ 𝑓 𝜒
42 nfv ⊢ Ⅎ 𝑓 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
43 41 42 nfan ⊢ Ⅎ 𝑓 ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
44 11 43 nfxfr ⊢ Ⅎ 𝑓 𝜃
45 nfv ⊢ Ⅎ 𝑓 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 )
46 nfv ⊢ Ⅎ 𝑓 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
47 44 45 46 nf3an ⊢ Ⅎ 𝑓 ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
48 12 47 nfxfr ⊢ Ⅎ 𝑓 𝜂
49 48 nf5ri ⊢ ( 𝜂 → ∀ 𝑓 𝜂 )
50 11 simplbi ⊢ ( 𝜃 → 𝜒 )
51 12 50 bnj835 ⊢ ( 𝜂 → 𝜒 )
52 12 simp2bi ⊢ ( 𝜂 → 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) )
53 1 2 3 4 5 6 7 8 bnj1388 ⊢ ( 𝜒 → ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∃ 𝑓 𝜏′ )
54 rsp ⊢ ( ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∃ 𝑓 𝜏′ → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ∃ 𝑓 𝜏′ ) )
55 53 54 syl ⊢ ( 𝜒 → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ∃ 𝑓 𝜏′ ) )
56 51 52 55 sylc ⊢ ( 𝜂 → ∃ 𝑓 𝜏′ )
57 49 56 bnj596 ⊢ ( 𝜂 → ∃ 𝑓 ( 𝜂 ∧ 𝜏′ ) )
58 1 2 3 4 8 bnj1373 ⊢ ( 𝜏′ ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
59 58 simplbi ⊢ ( 𝜏′ → 𝑓 ∈ 𝐶 )
60 59 adantl ⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑓 ∈ 𝐶 )
61 58 simprbi ⊢ ( 𝜏′ → dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
62 rspe ⊢ ( ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
63 52 61 62 syl2an ⊢ ( ( 𝜂 ∧ 𝜏′ ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
64 9 eqabri ⊢ ( 𝑓 ∈ 𝐻 ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ )
65 58 rexbii ⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
66 r19.42v ⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑓 ∈ 𝐶 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
67 64 65 66 3bitri ⊢ ( 𝑓 ∈ 𝐻 ↔ ( 𝑓 ∈ 𝐶 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
68 60 63 67 sylanbrc ⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑓 ∈ 𝐻 )
69 12 simp3bi ⊢ ( 𝜂 → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
70 69 adantr ⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
71 61 adantl ⊢ ( ( 𝜂 ∧ 𝜏′ ) → dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
72 70 71 eleqtrrd ⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑧 ∈ dom 𝑓 )
73 68 72 jca ⊢ ( ( 𝜂 ∧ 𝜏′ ) → ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
74 57 73 bnj593 ⊢ ( 𝜂 → ∃ 𝑓 ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
75 df-rex ⊢ ( ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 ↔ ∃ 𝑓 ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
76 74 75 sylibr ⊢ ( 𝜂 → ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
77 10 dmeqi ⊢ dom 𝑃 = dom ∪ 𝐻
78 9 bnj1317 ⊢ ( 𝑤 ∈ 𝐻 → ∀ 𝑓 𝑤 ∈ 𝐻 )
79 78 bnj1400 ⊢ dom ∪ 𝐻 = ∪ 𝑓 ∈ 𝐻 dom 𝑓
80 77 79 eqtri ⊢ dom 𝑃 = ∪ 𝑓 ∈ 𝐻 dom 𝑓
81 80 eleq2i ⊢ ( 𝑧 ∈ dom 𝑃 ↔ 𝑧 ∈ ∪ 𝑓 ∈ 𝐻 dom 𝑓 )
82 eliun ⊢ ( 𝑧 ∈ ∪ 𝑓 ∈ 𝐻 dom 𝑓 ↔ ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
83 81 82 bitri ⊢ ( 𝑧 ∈ dom 𝑃 ↔ ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
84 76 83 sylibr ⊢ ( 𝜂 → 𝑧 ∈ dom 𝑃 )
85 26 84 bnj593 ⊢ ( 𝜃 → ∃ 𝑦 𝑧 ∈ dom 𝑃 )
86 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′
87 86 nfab ⊢ Ⅎ 𝑦 { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
88 9 87 nfcxfr ⊢ Ⅎ 𝑦 𝐻
89 88 nfuni ⊢ Ⅎ 𝑦 ∪ 𝐻
90 10 89 nfcxfr ⊢ Ⅎ 𝑦 𝑃
91 90 nfdm ⊢ Ⅎ 𝑦 dom 𝑃
92 91 nfcrii ⊢ ( 𝑧 ∈ dom 𝑃 → ∀ 𝑦 𝑧 ∈ dom 𝑃 )
93 85 92 bnj1397 ⊢ ( 𝜃 → 𝑧 ∈ dom 𝑃 )
94 11 93 sylbir ⊢ ( ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → 𝑧 ∈ dom 𝑃 )
95 94 ex ⊢ ( 𝜒 → ( 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ dom 𝑃 ) )
96 95 ssrdv ⊢ ( 𝜒 → ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ dom 𝑃 )
97 simpr ⊢ ( ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) → 𝑧 ∈ dom 𝑓 )
98 67 simprbi ⊢ ( 𝑓 ∈ 𝐻 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
99 98 adantr ⊢ ( ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
100 r19.42v ⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑧 ∈ dom 𝑓 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
101 eleq2 ⊢ ( dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑧 ∈ dom 𝑓 ↔ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
102 101 biimpac ⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
103 102 reximi ⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
104 100 103 sylbir ⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
105 97 99 104 syl2anc ⊢ ( ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
106 105 rexlimiva ⊢ ( ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
107 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
108 106 83 107 3imtr4i ⊢ ( 𝑧 ∈ dom 𝑃 → 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
109 108 ssriv ⊢ dom 𝑃 ⊆ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
110 109 a1i ⊢ ( 𝜒 → dom 𝑃 ⊆ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
111 96 110 eqssd ⊢ ( 𝜒 → ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = dom 𝑃 )