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
|
abeq2i |
⊢ ( 𝑓 ∈ 𝐻 ↔ ∃ 𝑦 ∈ 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 𝑃 ) |